[isabelle-dev] NEWS: improved support for Isabelle/ML
traytel at in.tum.de
Tue Feb 18 17:36:06 CET 2014
Am 17.02.2014 14:14, schrieb Makarius:
> * Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for
> auxiliary ML files.
> This refers to Isabelle/56ebc4d4d008. It continues recent
> improvements of auxiliary file support.
> The IDE support for Isabelle/ML is already quite substantial, but with
> every step forward, I get 5 new ideas what else could be done. I am
> curious to hear what early-adopters and testers of the Isabelle
> repository say.
I've tried it out when working on what is now Isabelle/fd9ea8ae28f6. It
is really great to see the error messages where they belong to and to
have the type annotations everywhere now also in ML files (just as in
embedded Isabelle/ML blocks). The new colors are also nice ;-).
However, once I had to restart Isabelle as JEdit became quite
irresponsive (using almost 4GB of memory, forced GC didn't help). Maybe
I just hat too many ML files open (I usually don't close them once
opened) or my ML files are just too big: e.g.
~~/src/HOL/Tools/BNF/bnf_gfp.ML, although on a fresh start after opening
just this ML file the system is responsive (with some understandable
delay in displaying the markup, but instantly processing edits). Maybe
slightly lighter type annotations (at every constant/variable rather
than at every subterm) would dodge such problems?
More information about the isabelle-dev