# HG changeset patch
# User wenzelm
# Date 1375709350 -7200
# Node ID 930ce8eacb87b319e6c2aece86f2e8503b2c81b2
# Parent  e93d73b51fd0030d50a16bce9d26abffe495c8b7
tuned signature -- more uniform treatment of overlays as command mapping;

diff -r e93d73b51fd0 -r 930ce8eacb87 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Aug 05 15:03:52 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Aug 05 15:29:10 2013 +0200
@@ -9,7 +9,7 @@
 sig
   val timing: bool Unsynchronized.ref
   type node_header = string * Thy_Header.header * string list
-  type overlay = Document_ID.command * string * 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 |
@@ -68,7 +68,7 @@
  {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)};
+  overlays = Inttab.make_list overlays};
 
 val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]);
 val no_perspective = make_perspective (false, [], []);
@@ -135,7 +135,7 @@
 
 (* node edits and associated executions *)
 
-type overlay = Document_ID.command * string * string list;
+type overlay = Document_ID.command * (string * string list);
 
 datatype node_edit =
   Clear |
diff -r e93d73b51fd0 -r 930ce8eacb87 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Aug 05 15:03:52 2013 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Aug 05 15:29:10 2013 +0200
@@ -17,20 +17,43 @@
 
   /* overlays -- print functions with arguments */
 
-  type Overlay = (Command, String, List[String])
+  type Overlay = (Command, (String, List[String]))
 
   object Overlays
   {
-    val empty = new Overlays(Set.empty)
+    val empty = new Overlays(Map.empty)
   }
 
-  final class Overlays private(rep: Set[Overlay])
+  final class Overlays private(rep: Map[Command, List[(String, List[String])]])
   {
-    def + (o: Overlay) = new Overlays(rep + o)
-    def - (o: Overlay) = new Overlays(rep - o)
+    def commands: Set[Command] = rep.keySet
     def is_empty: Boolean = rep.isEmpty
-    def dest: List[Overlay] = rep.toList
-    def commands: Set[Command] = rep.iterator.map(x => x._1).toSet
+
+    def insert(cmd: Command, fn: (String, List[String])): Overlays =
+    {
+      val fns = rep.get(cmd) getOrElse Nil
+      if (fns.contains(fn)) this
+      else new Overlays(rep + (cmd -> (fn :: fns)))
+    }
+
+    def remove(cmd: Command, fn: (String, List[String])): Overlays =
+      rep.get(cmd) match {
+        case Some(fns) =>
+          if (fns.contains(fn)) {
+            fns.filterNot(_ == fn) match {
+              case Nil => new Overlays(rep - cmd)
+              case fns1 => new Overlays(rep + (cmd -> fns1))
+            }
+          }
+          else this
+        case None => this
+      }
+
+    def dest: List[Overlay] =
+      (for {
+        (cmd, fns) <- rep.iterator
+        fn <- fns
+      } yield (cmd, fn)).toList
   }
 
 
diff -r e93d73b51fd0 -r 930ce8eacb87 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Mon Aug 05 15:03:52 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML	Mon Aug 05 15:29:10 2013 +0200
@@ -58,7 +58,7 @@
                     in Document.Deps (master, header, errors) end,
                   fn (a :: b, c) =>
                     Document.Perspective (bool_atom a, map int_atom b,
-                      list (triple int string (list string)) c)]))
+                      list (pair int (pair string (list string))) c)]))
             end;
 
         val (removed, assign_update, state') = Document.update old_id new_id edits state;
diff -r e93d73b51fd0 -r 930ce8eacb87 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Aug 05 15:03:52 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala	Mon Aug 05 15:29:10 2013 +0200
@@ -342,7 +342,7 @@
                 (dir, (name.theory, (imports, (keywords, header.errors)))))) },
           { 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)) }))
+                list(pair(id, pair(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 e93d73b51fd0 -r 930ce8eacb87 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Aug 05 15:03:52 2013 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Aug 05 15:29:10 2013 +0200
@@ -81,11 +81,11 @@
 
   private var overlays = Document.Overlays.empty
 
-  def add_overlay(command: Command, name: String, args: List[String]): Unit =
-    Swing_Thread.require { overlays += ((command, name, args)) }
+  def insert_overlay(command: Command, name: String, args: List[String]): Unit =
+    Swing_Thread.require { overlays = overlays.insert(command, (name, args)) }
 
   def remove_overlay(command: Command, name: String, args: List[String]): Unit =
-    Swing_Thread.require { overlays -= ((command, name, args)) }
+    Swing_Thread.require { overlays = overlays.remove(command, (name, args)) }
 
 
   /* perspective */
diff -r e93d73b51fd0 -r 930ce8eacb87 src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Mon Aug 05 15:03:52 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Mon Aug 05 15:29:10 2013 +0200
@@ -114,7 +114,7 @@
           case Some(command) =>
             current_location = Some(command)
             current_query = query
-            doc_view.model.add_overlay(command, FIND_THEOREMS, List(instance, query))
+            doc_view.model.insert_overlay(command, FIND_THEOREMS, List(instance, query))
           case None =>
         }
       case None =>