--- a/NEWS Mon Jul 29 20:38:40 2013 +0200
+++ b/NEWS Mon Jul 29 20:46:21 2013 +0200
@@ -43,6 +43,12 @@
*** Prover IDE -- Isabelle/Scala/jEdit ***
+* 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".
+
* Strictly monotonic document update, without premature cancelation of
running transactions that are still needed: avoid reset/restart of
such command executions while editing.
--- a/etc/options Mon Jul 29 20:38:40 2013 +0200
+++ b/etc/options Mon Jul 29 20:46:21 2013 +0200
@@ -127,7 +127,7 @@
-- "execution priority of main document structure (e.g. 0, -1, -2)"
option editor_execution_range : string = "visible"
- -- "range of continuous document processing: all, none, visible"
+ -- "execution range of continuous document processing: all, none, visible"
section "Miscellaneous Tools"
--- a/src/Tools/jEdit/src/theories_dockable.scala Mon Jul 29 20:38:40 2013 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Mon Jul 29 20:46:21 2013 +0200
@@ -63,7 +63,7 @@
}
private val label =
new Label("Range:") { tooltip = "Execution range of continuous document processing" }
- private val b1 = button(PIDE.Execution_Range.ALL, "Check all theories")
+ private val b1 = button(PIDE.Execution_Range.ALL, "Check all theories (potentially slow)")
private val b2 = button(PIDE.Execution_Range.NONE, "Check nothing")
private val b3 = button(PIDE.Execution_Range.VISIBLE, "Check visible parts of theories")
private val group = new ButtonGroup(b1, b2, b3)