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