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