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

[Makarius]

On Tue, 1 Apr 2014, Dmitriy Traytel wrote:

>>    * The main portion of semantic ML markup is now maintained persistently
>>      in ML, and sent to the Scala side via some Execution.print function,
>>      which is asynchronous, depends on perspective, and non-persistent.
>>      This means, whenever some already processed ML file is visited in the
>>      editor, substantial amounts of reports are sent over the wire on the
>>      spot -- there is a deep purple flash seen on the ML_file command.
>>      When the file becomes invisible later, these resources are freed
>>  after
>>      some timeout and the JVM gets a chance to perform GC eventually.
>
> Do I understand the third bullet point correctly, in that closing ML buffers 
> is not required anymore (to save space), since the memory associated to 
> unfocused buffers will be freed by GC eventually?

Yes, and you can't even do anything to unload ML files that were open 
once.  The IDE data remains persistent within the ML process and is sent 
to the Scala side each time the file becomes (again) visible.


 	Makarius