# HG changeset patch # User wenzelm # Date 1375277047 -7200 # Node ID a39c5089b06eeed82d2b10945226a43447127afc # Parent 146ce45c36198a49933bd2202d220ce54169c74b# Parent dae6c61f991efcb27246b238ccba52ded267d6f2 merged diff -r 146ce45c3619 -r a39c5089b06e NEWS --- a/NEWS Wed Jul 31 13:40:57 2013 +0200 +++ b/NEWS Wed Jul 31 15:24:07 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 146ce45c3619 -r a39c5089b06e etc/options --- a/etc/options Wed Jul 31 13:40:57 2013 +0200 +++ b/etc/options Wed Jul 31 15:24:07 2013 +0200 @@ -123,15 +123,12 @@ 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 146ce45c3619 -r a39c5089b06e src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Wed Jul 31 13:40:57 2013 +0200 +++ b/src/Pure/PIDE/document.ML Wed Jul 31 15:24:07 2013 +0200 @@ -13,7 +13,7 @@ Clear | (* FIXME unused !? *) Edits of (Document_ID.command option * Document_ID.command option) list | Deps of node_header | - Perspective of Document_ID.command list + Perspective of bool * Document_ID.command list type edit = string * node_edit type state val init_state: state @@ -40,12 +40,12 @@ fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document_ID.print id); type node_header = string * Thy_Header.header * string list; -type perspective = Inttab.set * Document_ID.command option; +type perspective = bool * Inttab.set * Document_ID.command option; structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord); abstype node = Node of {header: node_header, (*master directory, theory header, errors*) - perspective: perspective, (*visible commands, last visible command*) + perspective: perspective, (*required node, visible commands, last visible command*) entries: Command.exec option Entries.T, (*command entries with excecutions*) result: Command.eval option} (*result of last execution*) and version = Version of node String_Graph.T (*development graph wrt. static imports*) @@ -57,11 +57,11 @@ fun map_node f (Node {header, perspective, entries, result}) = make_node (f (header, perspective, entries, result)); -fun make_perspective command_ids : perspective = - (Inttab.make_set command_ids, try List.last command_ids); +fun make_perspective (required, command_ids) : perspective = + (required, Inttab.make_set command_ids, try List.last command_ids); val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]); -val no_perspective = make_perspective []; +val no_perspective = make_perspective (false, []); val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE); val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, NONE)); @@ -83,11 +83,12 @@ in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords) end; fun get_perspective (Node {perspective, ...}) = perspective; -fun set_perspective ids = - map_node (fn (header, _, entries, result) => (header, make_perspective ids, entries, result)); +fun set_perspective args = + map_node (fn (header, _, entries, result) => (header, make_perspective args, entries, result)); -val visible_command = Inttab.defined o #1 o get_perspective; -val visible_last = #2 o get_perspective; +val required_node = #1 o get_perspective; +val visible_command = Inttab.defined o #2 o get_perspective; +val visible_last = #3 o get_perspective; val visible_node = is_some o visible_last fun map_entries f = @@ -127,7 +128,7 @@ Clear | Edits of (Document_ID.command option * Document_ID.command option) list | Deps of node_header | - Perspective of Document_ID.command list; + Perspective of bool * Document_ID.command list; type edit = string * node_edit; @@ -305,7 +306,6 @@ val {version_id, execution_id, delay_request, frontier} = execution; val delay = seconds (Options.default_real "editor_execution_delay"); - val pri = Options.default_int "editor_execution_priority"; val _ = Future.cancel delay_request; val delay_request' = Event_Timer.future (Time.+ (Time.now (), delay)); @@ -330,7 +330,7 @@ (singleton o Future.forks) {name = "theory:" ^ name, group = SOME (Future.new_group NONE), deps = more_deps @ map #2 (maps #2 deps), - pri = pri, interrupts = false} body; + pri = 0, interrupts = false} body; in [(name, Future.task_of future)] end else []); val frontier' = (fold o fold) Symtab.update new_tasks frontier; @@ -365,16 +365,18 @@ fun make_required nodes = let - val all_visible = - String_Graph.fold (fn (a, (node, _)) => visible_node node ? cons a) nodes [] + fun all_preds P = + String_Graph.fold (fn (a, (node, _)) => P node ? cons a) nodes [] |> String_Graph.all_preds nodes - |> map (rpair ()) |> Symtab.make; + |> Symtab.make_set; - val required = - Symtab.fold (fn (a, ()) => - exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ? - Symtab.update (a, ())) all_visible Symtab.empty; - in required end; + val all_visible = all_preds visible_node; + val all_required = all_preds required_node; + in + Symtab.fold (fn (a, ()) => + exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ? + Symtab.update (a, ())) all_visible all_required + end; fun init_theory deps node span = let diff -r 146ce45c3619 -r a39c5089b06e src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Wed Jul 31 13:40:57 2013 +0200 +++ b/src/Pure/PIDE/document.scala Wed Jul 31 15:24:07 2013 +0200 @@ -66,7 +66,8 @@ case class Clear[A, B]() extends Edit[A, B] case class Edits[A, B](edits: List[A]) extends Edit[A, B] case class Deps[A, B](header: Header) extends Edit[A, B] - case class Perspective[A, B](perspective: B) extends Edit[A, B] + case class Perspective[A, B](required: Boolean, perspective: B) extends Edit[A, B] + type Perspective_Text = Perspective[Text.Edit, Text.Perspective] def command_starts(commands: Iterator[Command], offset: Text.Offset = 0) : Iterator[(Command, Text.Offset)] = @@ -86,7 +87,7 @@ final class Node private( val header: Node.Header = Node.bad_header("Bad theory header"), - val perspective: Command.Perspective = Command.Perspective.empty, + val perspective: (Boolean, Command.Perspective) = (false, Command.Perspective.empty), val commands: Linear_Set[Command] = Linear_Set.empty) { def clear: Node = new Node(header = header) @@ -94,9 +95,12 @@ def update_header(new_header: Node.Header): Node = new Node(new_header, perspective, commands) - def update_perspective(new_perspective: Command.Perspective): Node = + def update_perspective(new_perspective: (Boolean, Command.Perspective)): Node = new Node(header, new_perspective, commands) + def same_perspective(other: (Boolean, Command.Perspective)): Boolean = + perspective._1 == other._1 && (perspective._2 same other._2) + def update_commands(new_commands: Linear_Set[Command]): Node = new Node(header, perspective, new_commands) diff -r 146ce45c3619 -r a39c5089b06e src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Wed Jul 31 13:40:57 2013 +0200 +++ b/src/Pure/PIDE/protocol.ML Wed Jul 31 15:24:07 2013 +0200 @@ -56,7 +56,7 @@ val imports' = map (rpair Position.none) imports; val header = Thy_Header.make (name, Position.none) imports' keywords; in Document.Deps (master, header, errors) end, - fn (a, []) => Document.Perspective (map int_atom a)])) + fn (a :: b, []) => Document.Perspective (bool_atom a, map int_atom b)])) end; val (removed, assign_update, state') = Document.update old_id new_id edits state; diff -r 146ce45c3619 -r a39c5089b06e src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Wed Jul 31 13:40:57 2013 +0200 +++ b/src/Pure/PIDE/protocol.scala Wed Jul 31 15:24:07 2013 +0200 @@ -340,7 +340,8 @@ option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))), list(Encode.string)))))( (dir, (name.theory, (imports, (keywords, header.errors)))))) }, - { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) })) + { case Document.Node.Perspective(a, b) => + (bool_atom(a) :: b.commands.map(c => long_atom(c.id)), Nil) })) def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) => { val (name, edit) = node_edit diff -r 146ce45c3619 -r a39c5089b06e src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Wed Jul 31 13:40:57 2013 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Wed Jul 31 15:24:07 2013 +0200 @@ -311,17 +311,17 @@ case (name, Document.Node.Edits(text_edits)) => val commands0 = node.commands val commands1 = edit_text(text_edits, commands0) - val commands2 = recover_spans(syntax, name, node.perspective, commands1) + val commands2 = recover_spans(syntax, name, node.perspective._2, commands1) node.update_commands(commands2) case (_, Document.Node.Deps(_)) => node - case (name, Document.Node.Perspective(text_perspective)) => - val perspective = command_perspective(node, text_perspective) - if (node.perspective same perspective) node + case (name, Document.Node.Perspective(required, text_perspective)) => + val perspective = (required, command_perspective(node, text_perspective)) + if (node.same_perspective(perspective)) node else node.update_perspective(perspective).update_commands( - consolidate_spans(syntax, reparse_limit, name, perspective, node.commands)) + consolidate_spans(syntax, reparse_limit, name, perspective._2, node.commands)) } } @@ -353,8 +353,9 @@ else node val node2 = (node1 /: edits)(text_edit(syntax, reparse_limit, _, _)) - if (!(node.perspective same node2.perspective)) - doc_edits += (name -> Document.Node.Perspective(node2.perspective)) + if (!(node.same_perspective(node2.perspective))) + doc_edits += + (name -> Document.Node.Perspective(node2.perspective._1, node2.perspective._2)) doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands))) diff -r 146ce45c3619 -r a39c5089b06e src/Pure/goal.ML --- a/src/Pure/goal.ML Wed Jul 31 13:40:57 2013 +0200 +++ b/src/Pure/goal.ML Wed Jul 31 15:24:07 2013 +0200 @@ -293,7 +293,7 @@ Term.exists_subterm Term.is_Var t orelse Term.exists_type (Term.exists_subtype Term.is_TVar) t; -fun prove_common immediate ctxt xs asms props tac = +fun prove_common immediate pri ctxt xs asms props tac = let val thy = Proof_Context.theory_of ctxt; val string_of_term = Syntax.string_of_term ctxt; @@ -337,7 +337,7 @@ val res = if immediate orelse schematic orelse not future orelse skip then result () - else future_result ctxt' (fork ~1 result) (Thm.term_of stmt); + else future_result ctxt' (fork pri result) (Thm.term_of stmt); in Conjunction.elim_balanced (length props) res |> map (Assumption.export false ctxt' ctxt) @@ -345,11 +345,14 @@ |> map Drule.zero_var_indexes end; -val prove_multi = prove_common true; +val prove_multi = prove_common true 0; -fun prove_future ctxt xs asms prop tac = hd (prove_common false ctxt xs asms [prop] tac); +fun prove_future_pri pri ctxt xs asms prop tac = + hd (prove_common false pri ctxt xs asms [prop] tac); -fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac); +val prove_future = prove_future_pri ~1; + +fun prove ctxt xs asms prop tac = hd (prove_multi ctxt xs asms [prop] tac); fun prove_global_future thy xs asms prop tac = Drule.export_without_context (prove_future (Proof_Context.init_global thy) xs asms prop tac); @@ -360,7 +363,7 @@ fun prove_sorry ctxt xs asms prop tac = if Config.get ctxt quick_and_dirty then prove ctxt xs asms prop (fn _ => ALLGOALS Skip_Proof.cheat_tac) - else (if future_enabled () then prove_future else prove) ctxt xs asms prop tac; + else (if future_enabled () then prove_future_pri ~2 else prove) ctxt xs asms prop tac; fun prove_sorry_global thy xs asms prop tac = Drule.export_without_context diff -r 146ce45c3619 -r a39c5089b06e src/Tools/jEdit/src/actions.xml --- a/src/Tools/jEdit/src/actions.xml Wed Jul 31 13:40:57 2013 +0200 +++ b/src/Tools/jEdit/src/actions.xml Wed Jul 31 15:24:07 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 146ce45c3619 -r a39c5089b06e src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Wed Jul 31 13:40:57 2013 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Wed Jul 31 15:24:07 2013 +0200 @@ -79,20 +79,23 @@ /* perspective */ - def node_perspective(): Text.Perspective = + var required_node = false + + def node_perspective(): Document.Node.Perspective_Text = { 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( + val perspective = + if (PIDE.continuous_checking) { + (required_node, Text.Perspective( for { doc_view <- PIDE.document_views(buffer) range <- doc_view.perspective().ranges - } yield range) - } + } yield range)) + } + else (false, Text.Perspective.empty) + + Document.Node.Perspective(perspective._1, perspective._2) } @@ -108,10 +111,10 @@ List(session.header_edit(name, header), name -> Document.Node.Clear(), name -> Document.Node.Edits(List(Text.Edit.insert(0, text))), - name -> Document.Node.Perspective(perspective)) + name -> perspective) } - def node_edits(perspective: Text.Perspective, text_edits: List[Text.Edit]) + def node_edits(perspective: Document.Node.Perspective_Text, text_edits: List[Text.Edit]) : List[Document.Edit_Text] = { Swing_Thread.require() @@ -119,7 +122,7 @@ List(session.header_edit(name, header), name -> Document.Node.Edits(text_edits), - name -> Document.Node.Perspective(perspective)) + name -> perspective) } @@ -128,7 +131,8 @@ private object pending_edits // owned by Swing thread { private val pending = new mutable.ListBuffer[Text.Edit] - private var last_perspective: Text.Perspective = Text.Perspective.empty + private var last_perspective: Document.Node.Perspective_Text = + Document.Node.Perspective(required_node, Text.Perspective.empty) def snapshot(): List[Text.Edit] = pending.toList diff -r 146ce45c3619 -r a39c5089b06e src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Wed Jul 31 13:40:57 2013 +0200 +++ b/src/Tools/jEdit/src/jEdit.props Wed Jul 31 15:24:07 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 146ce45c3619 -r a39c5089b06e src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Wed Jul 31 13:40:57 2013 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Wed Jul 31 15:24:07 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 146ce45c3619 -r a39c5089b06e src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Wed Jul 31 13:40:57 2013 +0200 +++ b/src/Tools/jEdit/src/theories_dockable.scala Wed Jul 31 15:24:07 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) @@ -101,6 +82,11 @@ var node_name = Document.Node.Name.empty override def paintComponent(gfx: Graphics2D) { + val size = peer.getSize() + val insets = border.getBorderInsets(peer) + val w = size.width - insets.left - insets.right + val h = size.height - insets.top - insets.bottom + nodes_status.get(node_name) match { case Some(st) if st.total > 0 => val colors = List( @@ -109,12 +95,7 @@ (st.warned, PIDE.options.color_value("warning_color")), (st.failed, PIDE.options.color_value("error_color"))) - val size = peer.getSize() - val insets = border.getBorderInsets(peer) - val w = size.width - insets.left - insets.right - val h = size.height - insets.top - insets.bottom var end = size.width - insets.right - for { (n, color) <- colors } { gfx.setColor(color) @@ -123,6 +104,8 @@ end = end - v - 1 } case _ => + gfx.setColor(PIDE.options.color_value("unprocessed1_color")) + gfx.fillRect(insets.left, insets.top, w, h) } super.paintComponent(gfx) } @@ -175,7 +158,7 @@ case _: Session.Global_Options => Swing_Thread.later { - execution_range.load() + continuous_checking.load() logic.load () }