[isabelle-dev] NEWS: improved support for Isabelle/ML

[Dmitriy Traytel]

Hi Makarius,

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?

Dmitriy