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

[Dmitriy Traytel]

This is really useful! Cf. e.g. 58b87aa4dc3b.

Sometimes there is distracting output by the "auto" tools: e.g. at 
http://isabelle.in.tum.de/repos/isabelle/file/58b87aa4dc3b/src/HOL/BNF/Examples/ListF.thy#l102 
a "Code generator: dropping subsumed code equation" by Auto Quickcheck 
and at 
http://isabelle.in.tum.de/repos/isabelle/file/58b87aa4dc3b/src/HOL/BNF/BNF_FP_Basic.thy#l38 
a unification trace from Auto solve_direct. I guess it would be the task 
the tools to omit such outbursts and not globally on the IDE side?

Dmitriy



Am 15.07.2013 11:54, schrieb 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>