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

[Makarius]

On Mon, 29 Jul 2013, Makarius wrote:

> * 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 has been superseded by Isabelle/76e9fbb7c080:

* Improved "Theories" panel: Continuous checking of proof document
(visible and required parts) may be controlled explicitly, using check
box or shortcut "C+e ENTER".  Individual theory nodes may be marked
explicitly as required and checked in full, using check box or
shortcut "C+e SPACE".


People hooked on the repository need to take care themselves that 
$ISABELLE_HOME_USER/jedit/keymaps/imported_keys.props is properly updated, 
e.g. by deleting the keymaps directory (with care!) and letting jedit do 
the implicit import from the global properties again.

The keyboard shortcuts "C+e ENTER" and "C+e SPACE" are somewhat 
reminiscent of ESCAPE META ALT CONTROL SHIFT.  It is important to 
understand the conceptual difference: these are not actions, to "drive" 
the prover, but declarative hints for the implicit proof checking process. 
(The system works like a TGV train in that respect, not like a handcart.)

Conceptually, I still need to clarify if the continuously running system 
can ever be "stopped", especially non-terminating attempts.  Right now, 
when continuous checking is deactivated, it will finish the frontier of 
running execution according to the monotonicity principle.  Hard 
interrupts no longer exist on reachable document sources -- they are not 
monotonic and spoil the parallel evaluation game.


Sun/Oracle have never deleted old stuff, so I had to spend most of the day 
studying the convoluted Java/Swing sources and API docs to get list views 
with additional GUI elements (check boxes).  The current implementation is 
just an optical illusion, and might break on very exotic look-and-feels.


 	Makarius