[isabelle-dev] NEWS: asynchronous print functions etc.

[Makarius]

* Strictly monotonic document update, without premature cancelation of
running transactions that are still needed: avoid reset/restart of
such command executions while editing.

* Support for asynchronous print functions, as overlay to existing
document content.

* Support for automatic tools in HOL, which try to prove or disprove
toplevel theorem statements.


This refers to Isabelle/9437f440ef3f.  Various refinements of the 
interactive document model (which had been in the pipeline for several 
years) now fit together to get the asynchronous "auto" tools on board. 
(There are some system options to switch them on or off, see the jEdit 
plugin options dialog.)

Note that there are still some snags with auto sledgehammer.  Apart from 
replacing the wrong command on clicking the result, I suspect that Stephan 
Schulz has sometimes problems terminating eprover cleanly when signalled 
via SIGINT.


 	Makarius