# HG changeset patch
# User wenzelm
# Date 1375446369 -7200
# Node ID 199e9fa5a5c2212c090853c47ec3f907e61740cc
# Parent  9489ca1d55dd714dd51d4f2e29fad887c280f4b1
maintain overlays within node perspective;
tuned signature;

diff -r 9489ca1d55dd -r 199e9fa5a5c2 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Aug 02 12:19:29 2013 +0200
+++ b/src/Pure/PIDE/command.scala	Fri Aug 02 14:26:09 2013 +0200
@@ -14,6 +14,9 @@
 
 object Command
 {
+  type Edit = (Option[Command], Option[Command])
+
+
   /** accumulated results from prover **/
 
   /* results */
diff -r 9489ca1d55dd -r 199e9fa5a5c2 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Aug 02 12:19:29 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Aug 02 14:26:09 2013 +0200
@@ -9,11 +9,12 @@
 sig
   val timing: bool Unsynchronized.ref
   type node_header = string * Thy_Header.header * string list
+  type overlay = Document_ID.command * string * string list
   datatype node_edit =
     Clear |    (* FIXME unused !? *)
     Edits of (Document_ID.command option * Document_ID.command option) list |
     Deps of node_header |
-    Perspective of bool * Document_ID.command list
+    Perspective of bool * Document_ID.command list * overlay list
   type edit = string * node_edit
   type state
   val init_state: state
@@ -40,12 +41,18 @@
 fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document_ID.print id);
 
 type node_header = string * Thy_Header.header * string list;
-type perspective = bool * Inttab.set * Document_ID.command option;
+
+type perspective =
+ {required: bool,  (*required node*)
+  visible: Inttab.set,  (*visible commands*)
+  visible_last: Document_ID.command option,  (*last visible command*)
+  overlays: (string * string list) list Inttab.table};  (*command id -> print function with args*)
+
 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,  (*required node, visible commands, last visible command*)
+  perspective: perspective,  (*command perspective*)
   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 +64,14 @@
 fun map_node f (Node {header, perspective, entries, result}) =
   make_node (f (header, perspective, entries, result));
 
-fun make_perspective (required, command_ids) : perspective =
-  (required, Inttab.make_set command_ids, try List.last command_ids);
+fun make_perspective (required, command_ids, overlays) : perspective =
+ {required = required,
+  visible = Inttab.make_set command_ids,
+  visible_last = try List.last command_ids,
+  overlays = Inttab.make_list (map (fn (x, y, z) => (x, (y, z))) overlays)};
 
 val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]);
-val no_perspective = make_perspective (false, []);
+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));
@@ -86,10 +96,11 @@
 fun set_perspective args =
   map_node (fn (header, _, entries, result) => (header, make_perspective args, entries, result));
 
-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 required_node = #required o get_perspective;
+val visible_command = Inttab.defined o #visible o get_perspective;
+val visible_last = #visible_last o get_perspective;
 val visible_node = is_some o visible_last
+val overlays = #overlays o get_perspective;
 
 fun map_entries f =
   map_node (fn (header, perspective, entries, result) => (header, perspective, f entries, result));
@@ -124,11 +135,13 @@
 
 (* node edits and associated executions *)
 
+type overlay = Document_ID.command * string * string list;
+
 datatype node_edit =
   Clear |
   Edits of (Document_ID.command option * Document_ID.command option) list |
   Deps of node_header |
-  Perspective of bool * Document_ID.command list;
+  Perspective of bool * Document_ID.command list * overlay list;
 
 type edit = string * node_edit;
 
diff -r 9489ca1d55dd -r 199e9fa5a5c2 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Aug 02 12:19:29 2013 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Aug 02 14:26:09 2013 +0200
@@ -15,11 +15,28 @@
 {
   /** document structure **/
 
+  /* overlays -- print functions with arguments */
+
+  type Overlay = (Command, String, List[String])
+
+  object Overlays
+  {
+    val empty = new Overlays(Set.empty)
+  }
+
+  final class Overlays private(rep: Set[Overlay])
+  {
+    def + (o: Overlay) = new Overlays(rep + o)
+    def - (o: Overlay) = new Overlays(rep - o)
+    def dest: List[Overlay] = rep.toList
+  }
+
+
   /* individual nodes */
 
   type Edit[A, B] = (Node.Name, Node.Edit[A, B])
   type Edit_Text = Edit[Text.Edit, Text.Perspective]
-  type Edit_Command = Edit[(Option[Command], Option[Command]), Command.Perspective]
+  type Edit_Command = Edit[Command.Edit, Command.Perspective]
 
   object Node
   {
@@ -66,8 +83,9 @@
     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](required: Boolean, perspective: B) extends Edit[A, B]
+    case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B]
     type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
+    type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
 
     def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
       : Iterator[(Command, Text.Offset)] =
@@ -87,7 +105,8 @@
 
   final class Node private(
     val header: Node.Header = Node.bad_header("Bad theory header"),
-    val perspective: (Boolean, Command.Perspective) = (false, Command.Perspective.empty),
+    val perspective: Node.Perspective_Command =
+      Node.Perspective(false, Command.Perspective.empty, Overlays.empty),
     val commands: Linear_Set[Command] = Linear_Set.empty)
   {
     def clear: Node = new Node(header = header)
@@ -95,11 +114,13 @@
     def update_header(new_header: Node.Header): Node =
       new Node(new_header, perspective, commands)
 
-    def update_perspective(new_perspective: (Boolean, Command.Perspective)): Node =
+    def update_perspective(new_perspective: Node.Perspective_Command): 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 same_perspective(other_perspective: Node.Perspective_Command): Boolean =
+      perspective.required == other_perspective.required &&
+      perspective.visible.same(other_perspective.visible) &&
+      perspective.overlays == other_perspective.overlays
 
     def update_commands(new_commands: Linear_Set[Command]): Node =
       new Node(header, perspective, new_commands)
diff -r 9489ca1d55dd -r 199e9fa5a5c2 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Fri Aug 02 12:19:29 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML	Fri Aug 02 14:26:09 2013 +0200
@@ -56,7 +56,9 @@
                       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 :: b, []) => Document.Perspective (bool_atom a, map int_atom b)]))
+                  fn (a :: b, c) =>
+                    Document.Perspective (bool_atom a, map int_atom b,
+                      list (triple int string (list string)) c)]))
             end;
 
         val (removed, assign_update, state') = Document.update old_id new_id edits state;
diff -r 9489ca1d55dd -r 199e9fa5a5c2 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Fri Aug 02 12:19:29 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala	Fri Aug 02 14:26:09 2013 +0200
@@ -326,7 +326,7 @@
     { import XML.Encode._
       def id: T[Command] = (cmd => long(cmd.id))
       def encode_edit(name: Document.Node.Name)
-          : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] =
+          : T[Document.Node.Edit[Command.Edit, Command.Perspective]] =
         variant(List(
           { case Document.Node.Clear() => (Nil, Nil) },  // FIXME unused !?
           { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
@@ -340,8 +340,9 @@
                     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, b) =>
-              (bool_atom(a) :: b.commands.map(c => long_atom(c.id)), Nil) }))
+          { case Document.Node.Perspective(a, b, c) =>
+              (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
+                list(triple(id, Encode.string, list(Encode.string)))(c.dest)) }))
       def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
       {
         val (name, edit) = node_edit
diff -r 9489ca1d55dd -r 199e9fa5a5c2 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Fri Aug 02 12:19:29 2013 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Fri Aug 02 14:26:09 2013 +0200
@@ -293,7 +293,7 @@
   /* main */
 
   def diff_commands(old_cmds: Linear_Set[Command], new_cmds: Linear_Set[Command])
-    : List[(Option[Command], Option[Command])] =
+    : List[Command.Edit] =
   {
     val removed = old_cmds.iterator.filter(!new_cmds.contains(_)).toList
     val inserted = new_cmds.iterator.filter(!old_cmds.contains(_)).toList
@@ -311,17 +311,18 @@
       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._2, commands1)
+        val commands2 = recover_spans(syntax, name, node.perspective.visible, commands1)
         node.update_commands(commands2)
 
       case (_, Document.Node.Deps(_)) => node
 
-      case (name, Document.Node.Perspective(required, text_perspective)) =>
-        val perspective = (required, command_perspective(node, text_perspective))
+      case (name, Document.Node.Perspective(required, text_perspective, overlays)) =>
+        val perspective: Document.Node.Perspective_Command =
+          Document.Node.Perspective(required, command_perspective(node, text_perspective), overlays)
         if (node.same_perspective(perspective)) node
         else
           node.update_perspective(perspective).update_commands(
-            consolidate_spans(syntax, reparse_limit, name, perspective._2, node.commands))
+            consolidate_spans(syntax, reparse_limit, name, perspective.visible, node.commands))
     }
   }
 
@@ -354,8 +355,7 @@
         val node2 = (node1 /: edits)(text_edit(syntax, reparse_limit, _, _))
 
         if (!(node.same_perspective(node2.perspective)))
-          doc_edits +=
-            (name -> Document.Node.Perspective(node2.perspective._1, node2.perspective._2))
+          doc_edits += (name -> node2.perspective)
 
         doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
 
diff -r 9489ca1d55dd -r 199e9fa5a5c2 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Fri Aug 02 12:19:29 2013 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Aug 02 14:26:09 2013 +0200
@@ -77,8 +77,28 @@
   }
 
 
+  /* overlays */
+
+  private var overlays = Document.Overlays.empty
+
+  def add_overlay(command: Command, name: String, args: List[String])
+  {
+    Swing_Thread.required()
+    overlays += ((command, name, args))
+    PIDE.flush_buffers()
+  }
+
+  def remove_overlay(command: Command, name: String, args: List[String])
+  {
+    Swing_Thread.required()
+    overlays -= ((command, name, args))
+    PIDE.flush_buffers()
+  }
+
+
   /* perspective */
 
+  // owned by Swing thread
   private var _node_required = false
   def node_required: Boolean = _node_required
   def node_required_=(b: Boolean)
@@ -91,21 +111,21 @@
     }
   }
 
+  val empty_perspective: Document.Node.Perspective_Text =
+    Document.Node.Perspective(false, Text.Perspective.empty, Document.Overlays.empty)
+
   def node_perspective(): Document.Node.Perspective_Text =
   {
     Swing_Thread.require()
 
-    val perspective =
-      if (Isabelle.continuous_checking) {
-        (node_required, 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)
+    if (Isabelle.continuous_checking) {
+      Document.Node.Perspective(node_required, Text.Perspective(
+        for {
+          doc_view <- PIDE.document_views(buffer)
+          range <- doc_view.perspective().ranges
+        } yield range), overlays)
+    }
+    else empty_perspective
   }
 
 
@@ -143,8 +163,7 @@
   private object pending_edits  // owned by Swing thread
   {
     private val pending = new mutable.ListBuffer[Text.Edit]
-    private var last_perspective: Document.Node.Perspective_Text =
-      Document.Node.Perspective(node_required, Text.Perspective.empty)
+    private var last_perspective = empty_perspective
 
     def snapshot(): List[Text.Edit] = pending.toList