[isabelle-dev] NEWS: execution range of continuous document processing

Makarius makarius at sketis.net
Mon Jul 29 21:42:30 CEST 2013


* Execution range of continuous document processing may be set to
"all", "none", "visible".  See also dockable window "Theories" or
keyboard shortcuts "C-e BACK_SPACE" for "none", and "C-e SPACE" for
"visible".  These declarative options supersede the old-style action
buttons "Cancel" and "Check".


This refers to Isabelle/82707f95a783.  It is just a stepping stone of 
various ongoing refinements of the document model and its interactive 
behaviour (i.e. the Prover IDE as computer game).

Early adopters are welcome to give feedback at any point, although I am 
aware that it is quite difficult to do so via email.  (At the ITP 
conference I've seen many fine points watching over the shoulders of 
Isabelle/jEdit users just for a few minutes, instead of struggling for 
myself in isolation.)

Users of "airy" machines might try a bit with the "none" option, and with 
manual configuration of the "threads" option to the actual number of cores 
(without the doubling due to hyperthreading).


 	Makarius


More information about the isabelle-dev mailing list