# HG changeset patch
# User wenzelm
# Date 1375123581 -7200
# Node ID 82707f95a7839abda0eade9198216e5f36a5ffdb
# Parent  19fa3e3964f068d63e3895722a3dc0df17d20d12
NEWS;
tuned description;

diff -r 19fa3e3964f0 -r 82707f95a783 NEWS
--- 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.
diff -r 19fa3e3964f0 -r 82707f95a783 etc/options
--- 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"
diff -r 19fa3e3964f0 -r 82707f95a783 src/Tools/jEdit/src/theories_dockable.scala
--- 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)