simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints);

--- a/NEWS	Tue Jul 30 23:17:26 2013 +0200
+++ b/NEWS	Wed Jul 31 10:54:37 2013 +0200
@@ -43,11 +43,8 @@
 
 *** 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".
+* Continuous checking of proof document (visible and required parts)
+may be controlled explicitly, using check box or "C+e ENTER" shortcut.
 
 * Strictly monotonic document update, without premature cancelation of
 running transactions that are still needed: avoid reset/restart of

--- a/etc/options	Tue Jul 30 23:17:26 2013 +0200
+++ b/etc/options	Wed Jul 31 10:54:37 2013 +0200
@@ -123,15 +123,15 @@
 public option editor_chart_delay : real = 3.0
   -- "delay for chart repainting"
 
+public option editor_continuous_checking : bool = true
+  -- "continuous checking of proof document (visible and required parts)"
+
 option editor_execution_delay : real = 0.02
   -- "delay for start of execution process after document update (seconds)"
 
 option editor_execution_priority : int = -1
   -- "execution priority of main document structure (e.g. 0, -1, -2)"
 
-option editor_execution_range : string = "visible"
-  -- "execution range of continuous document processing: all, none, visible"
-
 
 section "Miscellaneous Tools"
 

--- a/src/Tools/jEdit/src/actions.xml	Tue Jul 30 23:17:26 2013 +0200
+++ b/src/Tools/jEdit/src/actions.xml	Wed Jul 31 10:54:37 2013 +0200
@@ -52,14 +52,19 @@
 			wm.addDockableWindow("isabelle-symbols");
 		</CODE>
 	</ACTION>
-	<ACTION NAME="isabelle.execution-range-none">
+	<ACTION NAME="isabelle.set-continuous-checking">
 	  <CODE>
-	    isabelle.jedit.PIDE.execution_range_none();
+	    isabelle.jedit.PIDE.set_continuous_checking();
 	  </CODE>
 	</ACTION>
-	<ACTION NAME="isabelle.execution-range-visible">
+	<ACTION NAME="isabelle.reset-continuous-checking">
 	  <CODE>
-	    isabelle.jedit.PIDE.execution_range_visible();
+	    isabelle.jedit.PIDE.reset_continuous_checking();
+	  </CODE>
+	</ACTION>
+	<ACTION NAME="isabelle.toggle-continuous-checking">
+	  <CODE>
+	    isabelle.jedit.PIDE.toggle_continuous_checking();
 	  </CODE>
 	</ACTION>
 	<ACTION NAME="isabelle.increase-font-size">

--- a/src/Tools/jEdit/src/document_model.scala	Tue Jul 30 23:17:26 2013 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Jul 31 10:54:37 2013 +0200
@@ -83,16 +83,14 @@
   {
     Swing_Thread.require()
 
-    PIDE.execution_range() match {
-      case PIDE.Execution_Range.ALL => Text.Perspective.full
-      case PIDE.Execution_Range.NONE => Text.Perspective.empty
-      case PIDE.Execution_Range.VISIBLE =>
-        Text.Perspective(
-          for {
-            doc_view <- PIDE.document_views(buffer)
-            range <- doc_view.perspective().ranges
-          } yield range)
+    if (PIDE.continuous_checking) {
+      Text.Perspective(
+        for {
+          doc_view <- PIDE.document_views(buffer)
+          range <- doc_view.perspective().ranges
+        } yield range)
     }
+    else Text.Perspective.empty
   }
 
 

--- a/src/Tools/jEdit/src/jEdit.props	Tue Jul 30 23:17:26 2013 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Wed Jul 31 10:54:37 2013 +0200
@@ -185,10 +185,10 @@
 isabelle-readme.dock-position=bottom
 isabelle-symbols.dock-position=bottom
 isabelle-theories.dock-position=right
-isabelle.execution-range-none.label=Check nothing
-isabelle.execution-range-none.shortcut=C+e BACK_SPACE
-isabelle.execution-range-visible=Check visible parts of theories
-isabelle.execution-range-visible.shortcut=C+e SPACE
+isabelle.set-continuous-checking.label=Enable continuous checking
+isabelle.reset-continuous-checking.label=Disable continuous checking
+isabelle.toggle-continuous-checking.label=Toggle continuous checking
+isabelle.toggle-continuous-checking.shortcut=C+e ENTER
 isabelle.control-bold.label=Control bold
 isabelle.control-bold.shortcut=C+e RIGHT
 isabelle.control-isub.label=Control subscript

--- a/src/Tools/jEdit/src/plugin.scala	Tue Jul 30 23:17:26 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Jul 31 10:54:37 2013 +0200
@@ -117,28 +117,18 @@
   }
 
 
-  /* execution range */
+  /* continuous checking */
 
-  object Execution_Range extends Enumeration {
-    val ALL = Value("all")
-    val NONE = Value("none")
-    val VISIBLE = Value("visible")
-  }
+  private val CONTINUOUS_CHECKING = "editor_continuous_checking"
 
-  def execution_range(): Execution_Range.Value =
-    options.string("editor_execution_range") match {
-      case "all" => Execution_Range.ALL
-      case "none" => Execution_Range.NONE
-      case "visible" => Execution_Range.VISIBLE
-      case s => error("Bad value for option \"editor_execution_range\": " + quote(s))
-    }
+  def continuous_checking: Boolean = options.bool(CONTINUOUS_CHECKING)
 
-  def update_execution_range(range: Execution_Range.Value)
+  def continuous_checking_=(b: Boolean)
   {
     Swing_Thread.require()
 
-    if (options.string("editor_execution_range") != range.toString) {
-      options.string("editor_execution_range") = range.toString
+    if (continuous_checking != b) {
+      options.bool(CONTINUOUS_CHECKING) = b
       PIDE.session.global_options.event(Session.Global_Options(options.value))
 
       PIDE.session.update(
@@ -155,8 +145,9 @@
     }
   }
 
-  def execution_range_none(): Unit = update_execution_range(Execution_Range.NONE)
-  def execution_range_visible(): Unit = update_execution_range(Execution_Range.VISIBLE)
+  def set_continuous_checking() { continuous_checking = true }
+  def reset_continuous_checking() { continuous_checking = false }
+  def toggle_continuous_checking() { continuous_checking = !continuous_checking }
 }
 
 

--- a/src/Tools/jEdit/src/theories_dockable.scala	Tue Jul 30 23:17:26 2013 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 31 10:54:37 2013 +0200
@@ -10,8 +10,8 @@
 import isabelle._
 
 import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component,
-  BoxPanel, Orientation, RadioButton, ButtonGroup}
+import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment,
+  ScrollPane, Component, CheckBox}
 import scala.swing.event.{ButtonClicked, MouseClicked}
 
 import java.lang.System
@@ -55,36 +55,17 @@
     Swing_Thread.later { session_phase.text = " " + phase_text(phase) + " " }
   }
 
-  private val execution_range = new BoxPanel(Orientation.Horizontal) {
-    private def button(range: PIDE.Execution_Range.Value, tip: String): RadioButton =
-      new RadioButton(range.toString) {
-        tooltip = tip
-        reactions += { case ButtonClicked(_) => PIDE.update_execution_range(range) }
-      }
-    private val label =
-      new Label("Range:") { tooltip = "Execution range of continuous document processing" }
-    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)
-    contents ++= List(label, b1, b2, b3)
-    border = new SoftBevelBorder(BevelBorder.LOWERED)
-
-    def load()
-    {
-      PIDE.execution_range() match {
-        case PIDE.Execution_Range.ALL => group.select(b1)
-        case PIDE.Execution_Range.NONE => group.select(b2)
-        case PIDE.Execution_Range.VISIBLE => group.select(b3)
-      }
-    }
+  private val continuous_checking = new CheckBox("Continuous checking") {
+    tooltip = "Continuous checking of proof document (visible and required parts)"
+    reactions += { case ButtonClicked(_) => PIDE.continuous_checking = selected }
+    def load() { selected = PIDE.continuous_checking }
     load()
   }
 
   private val logic = Isabelle_Logic.logic_selector(true)
 
   private val controls =
-    new FlowPanel(FlowPanel.Alignment.Right)(execution_range, session_phase, logic)
+    new FlowPanel(FlowPanel.Alignment.Right)(continuous_checking, session_phase, logic)
   add(controls.peer, BorderLayout.NORTH)
 
 
@@ -175,7 +156,7 @@
 
         case _: Session.Global_Options =>
           Swing_Thread.later {
-            execution_range.load()
+            continuous_checking.load()
             logic.load ()
           }