# HG changeset patch
# User wenzelm
# Date 1375265653 -7200
# Node ID 143f225e50f5861d1e7b8d42f8fd5146b044d47e
# Parent  b859a180936bf39150074229781c6d327bb9b4a6
allow explicit indication of required node: full eval, no prints;

diff -r b859a180936b -r 143f225e50f5 src/Pure/PIDE/document.ML
--- 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
diff -r b859a180936b -r 143f225e50f5 src/Pure/PIDE/document.scala
--- 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)
 
diff -r b859a180936b -r 143f225e50f5 src/Pure/PIDE/protocol.ML
--- 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;
diff -r b859a180936b -r 143f225e50f5 src/Pure/PIDE/protocol.scala
--- 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
diff -r b859a180936b -r 143f225e50f5 src/Pure/Thy/thy_syntax.scala
--- 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)))
 
diff -r b859a180936b -r 143f225e50f5 src/Tools/jEdit/src/document_model.scala
--- 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