--- 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
--- 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"
--- 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
--- 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)
--- 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;
--- 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
--- 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)))
--- 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
--- 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");
</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 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
--- 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
--- 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 }
}
--- 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 ()
}