1.1 --- a/NEWS	Tue Jul 30 23:17:26 2013 +0200
     1.2 +++ b/NEWS	Wed Jul 31 10:54:37 2013 +0200
     1.3 @@ -43,11 +43,8 @@
     1.4  
     1.5  *** Prover IDE -- Isabelle/Scala/jEdit ***
     1.6  
     1.7 -* Execution range of continuous document processing may be set to
     1.8 -"all", "none", "visible".  See also dockable window "Theories" or
     1.9 -keyboard shortcuts "C-e BACK_SPACE" for "none", and "C-e SPACE" for
    1.10 -"visible".  These declarative options supersede the old-style action
    1.11 -buttons "Cancel" and "Check".
    1.12 +* Continuous checking of proof document (visible and required parts)
    1.13 +may be controlled explicitly, using check box or "C+e ENTER" shortcut.
    1.14  
    1.15  * Strictly monotonic document update, without premature cancelation of
    1.16  running transactions that are still needed: avoid reset/restart of

     2.1 --- a/etc/options	Tue Jul 30 23:17:26 2013 +0200
     2.2 +++ b/etc/options	Wed Jul 31 10:54:37 2013 +0200
     2.3 @@ -123,15 +123,15 @@
     2.4  public option editor_chart_delay : real = 3.0
     2.5    -- "delay for chart repainting"
     2.6  
     2.7 +public option editor_continuous_checking : bool = true
     2.8 +  -- "continuous checking of proof document (visible and required parts)"
     2.9 +
    2.10  option editor_execution_delay : real = 0.02
    2.11    -- "delay for start of execution process after document update (seconds)"
    2.12  
    2.13  option editor_execution_priority : int = -1
    2.14    -- "execution priority of main document structure (e.g. 0, -1, -2)"
    2.15  
    2.16 -option editor_execution_range : string = "visible"
    2.17 -  -- "execution range of continuous document processing: all, none, visible"
    2.18 -
    2.19  
    2.20  section "Miscellaneous Tools"
    2.21  

     3.1 --- a/src/Tools/jEdit/src/actions.xml	Tue Jul 30 23:17:26 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/actions.xml	Wed Jul 31 10:54:37 2013 +0200
     3.3 @@ -52,14 +52,19 @@
     3.4  			wm.addDockableWindow("isabelle-symbols");
     3.5  		</CODE>
     3.6  	</ACTION>
     3.7 -	<ACTION NAME="isabelle.execution-range-none">
     3.8 +	<ACTION NAME="isabelle.set-continuous-checking">
     3.9  	  <CODE>
    3.10 -	    isabelle.jedit.PIDE.execution_range_none();
    3.11 +	    isabelle.jedit.PIDE.set_continuous_checking();
    3.12  	  </CODE>
    3.13  	</ACTION>
    3.14 -	<ACTION NAME="isabelle.execution-range-visible">
    3.15 +	<ACTION NAME="isabelle.reset-continuous-checking">
    3.16  	  <CODE>
    3.17 -	    isabelle.jedit.PIDE.execution_range_visible();
    3.18 +	    isabelle.jedit.PIDE.reset_continuous_checking();
    3.19 +	  </CODE>
    3.20 +	</ACTION>
    3.21 +	<ACTION NAME="isabelle.toggle-continuous-checking">
    3.22 +	  <CODE>
    3.23 +	    isabelle.jedit.PIDE.toggle_continuous_checking();
    3.24  	  </CODE>
    3.25  	</ACTION>
    3.26  	<ACTION NAME="isabelle.increase-font-size">

     4.1 --- a/src/Tools/jEdit/src/document_model.scala	Tue Jul 30 23:17:26 2013 +0200
     4.2 +++ b/src/Tools/jEdit/src/document_model.scala	Wed Jul 31 10:54:37 2013 +0200
     4.3 @@ -83,16 +83,14 @@
     4.4    {
     4.5      Swing_Thread.require()
     4.6  
     4.7 -    PIDE.execution_range() match {
     4.8 -      case PIDE.Execution_Range.ALL => Text.Perspective.full
     4.9 -      case PIDE.Execution_Range.NONE => Text.Perspective.empty
    4.10 -      case PIDE.Execution_Range.VISIBLE =>
    4.11 -        Text.Perspective(
    4.12 -          for {
    4.13 -            doc_view <- PIDE.document_views(buffer)
    4.14 -            range <- doc_view.perspective().ranges
    4.15 -          } yield range)
    4.16 +    if (PIDE.continuous_checking) {
    4.17 +      Text.Perspective(
    4.18 +        for {
    4.19 +          doc_view <- PIDE.document_views(buffer)
    4.20 +          range <- doc_view.perspective().ranges
    4.21 +        } yield range)
    4.22      }
    4.23 +    else Text.Perspective.empty
    4.24    }
    4.25  
    4.26  

     5.1 --- a/src/Tools/jEdit/src/jEdit.props	Tue Jul 30 23:17:26 2013 +0200
     5.2 +++ b/src/Tools/jEdit/src/jEdit.props	Wed Jul 31 10:54:37 2013 +0200
     5.3 @@ -185,10 +185,10 @@
     5.4  isabelle-readme.dock-position=bottom
     5.5  isabelle-symbols.dock-position=bottom
     5.6  isabelle-theories.dock-position=right
     5.7 -isabelle.execution-range-none.label=Check nothing
     5.8 -isabelle.execution-range-none.shortcut=C+e BACK_SPACE
     5.9 -isabelle.execution-range-visible=Check visible parts of theories
    5.10 -isabelle.execution-range-visible.shortcut=C+e SPACE
    5.11 +isabelle.set-continuous-checking.label=Enable continuous checking
    5.12 +isabelle.reset-continuous-checking.label=Disable continuous checking
    5.13 +isabelle.toggle-continuous-checking.label=Toggle continuous checking
    5.14 +isabelle.toggle-continuous-checking.shortcut=C+e ENTER
    5.15  isabelle.control-bold.label=Control bold
    5.16  isabelle.control-bold.shortcut=C+e RIGHT
    5.17  isabelle.control-isub.label=Control subscript

     6.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Jul 30 23:17:26 2013 +0200
     6.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Jul 31 10:54:37 2013 +0200
     6.3 @@ -117,28 +117,18 @@
     6.4    }
     6.5  
     6.6  
     6.7 -  /* execution range */
     6.8 +  /* continuous checking */
     6.9  
    6.10 -  object Execution_Range extends Enumeration {
    6.11 -    val ALL = Value("all")
    6.12 -    val NONE = Value("none")
    6.13 -    val VISIBLE = Value("visible")
    6.14 -  }
    6.15 +  private val CONTINUOUS_CHECKING = "editor_continuous_checking"
    6.16  
    6.17 -  def execution_range(): Execution_Range.Value =
    6.18 -    options.string("editor_execution_range") match {
    6.19 -      case "all" => Execution_Range.ALL
    6.20 -      case "none" => Execution_Range.NONE
    6.21 -      case "visible" => Execution_Range.VISIBLE
    6.22 -      case s => error("Bad value for option \"editor_execution_range\": " + quote(s))
    6.23 -    }
    6.24 +  def continuous_checking: Boolean = options.bool(CONTINUOUS_CHECKING)
    6.25  
    6.26 -  def update_execution_range(range: Execution_Range.Value)
    6.27 +  def continuous_checking_=(b: Boolean)
    6.28    {
    6.29      Swing_Thread.require()
    6.30  
    6.31 -    if (options.string("editor_execution_range") != range.toString) {
    6.32 -      options.string("editor_execution_range") = range.toString
    6.33 +    if (continuous_checking != b) {
    6.34 +      options.bool(CONTINUOUS_CHECKING) = b
    6.35        PIDE.session.global_options.event(Session.Global_Options(options.value))
    6.36  
    6.37        PIDE.session.update(
    6.38 @@ -155,8 +145,9 @@
    6.39      }
    6.40    }
    6.41  
    6.42 -  def execution_range_none(): Unit = update_execution_range(Execution_Range.NONE)
    6.43 -  def execution_range_visible(): Unit = update_execution_range(Execution_Range.VISIBLE)
    6.44 +  def set_continuous_checking() { continuous_checking = true }
    6.45 +  def reset_continuous_checking() { continuous_checking = false }
    6.46 +  def toggle_continuous_checking() { continuous_checking = !continuous_checking }
    6.47  }
    6.48  
    6.49  

     7.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Tue Jul 30 23:17:26 2013 +0200
     7.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 31 10:54:37 2013 +0200
     7.3 @@ -10,8 +10,8 @@
     7.4  import isabelle._
     7.5  
     7.6  import scala.actors.Actor._
     7.7 -import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component,
     7.8 -  BoxPanel, Orientation, RadioButton, ButtonGroup}
     7.9 +import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment,
    7.10 +  ScrollPane, Component, CheckBox}
    7.11  import scala.swing.event.{ButtonClicked, MouseClicked}
    7.12  
    7.13  import java.lang.System
    7.14 @@ -55,36 +55,17 @@
    7.15      Swing_Thread.later { session_phase.text = " " + phase_text(phase) + " " }
    7.16    }
    7.17  
    7.18 -  private val execution_range = new BoxPanel(Orientation.Horizontal) {
    7.19 -    private def button(range: PIDE.Execution_Range.Value, tip: String): RadioButton =
    7.20 -      new RadioButton(range.toString) {
    7.21 -        tooltip = tip
    7.22 -        reactions += { case ButtonClicked(_) => PIDE.update_execution_range(range) }
    7.23 -      }
    7.24 -    private val label =
    7.25 -      new Label("Range:") { tooltip = "Execution range of continuous document processing" }
    7.26 -    private val b1 = button(PIDE.Execution_Range.ALL, "Check all theories (potentially slow)")
    7.27 -    private val b2 = button(PIDE.Execution_Range.NONE, "Check nothing")
    7.28 -    private val b3 = button(PIDE.Execution_Range.VISIBLE, "Check visible parts of theories")
    7.29 -    private val group = new ButtonGroup(b1, b2, b3)
    7.30 -    contents ++= List(label, b1, b2, b3)
    7.31 -    border = new SoftBevelBorder(BevelBorder.LOWERED)
    7.32 -
    7.33 -    def load()
    7.34 -    {
    7.35 -      PIDE.execution_range() match {
    7.36 -        case PIDE.Execution_Range.ALL => group.select(b1)
    7.37 -        case PIDE.Execution_Range.NONE => group.select(b2)
    7.38 -        case PIDE.Execution_Range.VISIBLE => group.select(b3)
    7.39 -      }
    7.40 -    }
    7.41 +  private val continuous_checking = new CheckBox("Continuous checking") {
    7.42 +    tooltip = "Continuous checking of proof document (visible and required parts)"
    7.43 +    reactions += { case ButtonClicked(_) => PIDE.continuous_checking = selected }
    7.44 +    def load() { selected = PIDE.continuous_checking }
    7.45      load()
    7.46    }
    7.47  
    7.48    private val logic = Isabelle_Logic.logic_selector(true)
    7.49  
    7.50    private val controls =
    7.51 -    new FlowPanel(FlowPanel.Alignment.Right)(execution_range, session_phase, logic)
    7.52 +    new FlowPanel(FlowPanel.Alignment.Right)(continuous_checking, session_phase, logic)
    7.53    add(controls.peer, BorderLayout.NORTH)
    7.54  
    7.55  
    7.56 @@ -175,7 +156,7 @@
    7.57  
    7.58          case _: Session.Global_Options =>
    7.59            Swing_Thread.later {
    7.60 -            execution_range.load()
    7.61 +            continuous_checking.load()
    7.62              logic.load ()
    7.63            }
    7.64