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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
