# HG changeset patch # User wenzelm # Date 1375260877 -7200 # Node ID b859a180936bf39150074229781c6d327bb9b4a6 # Parent add5c023ba03cd2df2c270aa324639c9c9c81c38 simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints); diff -r add5c023ba03 -r b859a180936b NEWS --- 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 diff -r add5c023ba03 -r b859a180936b etc/options --- 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" diff -r add5c023ba03 -r b859a180936b src/Tools/jEdit/src/actions.xml --- 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"); - +


-	    isabelle.jedit.PIDE.execution_range_none();
+	    isabelle.jedit.PIDE.set_continuous_checking();

- +


-	    isabelle.jedit.PIDE.execution_range_visible();
+	    isabelle.jedit.PIDE.reset_continuous_checking();
+

+ + +


+	    isabelle.jedit.PIDE.toggle_continuous_checking();

diff -r add5c023ba03 -r b859a180936b src/Tools/jEdit/src/document_model.scala --- 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 } diff -r add5c023ba03 -r b859a180936b src/Tools/jEdit/src/jEdit.props --- 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 diff -r add5c023ba03 -r b859a180936b src/Tools/jEdit/src/plugin.scala --- 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 } } diff -r add5c023ba03 -r b859a180936b src/Tools/jEdit/src/theories_dockable.scala --- 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 () }