--- a/src/Pure/PIDE/document.ML Wed Jul 31 10:54:37 2013 +0200
+++ b/src/Pure/PIDE/document.ML Wed Jul 31 12:14:13 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;
@@ -365,16 +366,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 10:54:37 2013 +0200
+++ b/src/Pure/PIDE/document.scala Wed Jul 31 12:14:13 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 10:54:37 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML Wed Jul 31 12:14:13 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 10:54:37 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala Wed Jul 31 12:14:13 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 10:54:37 2013 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Wed Jul 31 12:14:13 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/Tools/jEdit/src/document_model.scala Wed Jul 31 10:54:37 2013 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Wed Jul 31 12:14:13 2013 +0200
@@ -79,18 +79,23 @@
/* perspective */
- def node_perspective(): Text.Perspective =
+ var required_node = false
+
+ def node_perspective(): Document.Node.Perspective_Text =
{
Swing_Thread.require()
- if (PIDE.continuous_checking) {
- Text.Perspective(
- for {
- doc_view <- PIDE.document_views(buffer)
- range <- doc_view.perspective().ranges
- } yield range)
- }
- else Text.Perspective.empty
+ val perspective =
+ if (PIDE.continuous_checking) {
+ (required_node, Text.Perspective(
+ for {
+ doc_view <- PIDE.document_views(buffer)
+ range <- doc_view.perspective().ranges
+ } yield range))
+ }
+ else (false, Text.Perspective.empty)
+
+ Document.Node.Perspective(perspective._1, perspective._2)
}
@@ -106,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()
@@ -117,7 +122,7 @@
List(session.header_edit(name, header),
name -> Document.Node.Edits(text_edits),
- name -> Document.Node.Perspective(perspective))
+ name -> perspective)
}
@@ -126,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