central management of Document.Overlays, independent of Document_Model;

--- a/src/Pure/PIDE/document.scala	Mon Aug 12 13:32:26 2013 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Aug 12 14:27:58 2013 +0200
@@ -15,6 +15,32 @@
 {
   /** document structure **/
 
+  /* overlays -- print functions with arguments */
+
+  object Overlays
+  {
+    val empty = new Overlays(Map.empty)
+  }
+
+  final class Overlays private(rep: Map[Node.Name, Node.Overlays])
+  {
+    def apply(name: Document.Node.Name): Node.Overlays =
+      rep.getOrElse(name, Node.Overlays.empty)
+
+    private def update(name: Node.Name, f: Node.Overlays => Node.Overlays): Overlays =
+    {
+      val node_overlays = f(apply(name))
+      new Overlays(if (node_overlays.is_empty) rep - name else rep + (name -> node_overlays))
+    }
+
+    def insert(command: Command, fn: String, args: List[String]): Overlays =
+      update(command.node_name, _.insert(command, fn, args))
+
+    def remove(command: Command, fn: String, args: List[String]): Overlays =
+      update(command.node_name, _.remove(command, fn, args))
+  }
+
+
   /* individual nodes */
 
   type Edit[A, B] = (Node.Name, Node.Edit[A, B])
@@ -60,27 +86,22 @@
     }
 
 
-    /* overlays -- print functions with arguments */
-
-    type Print_Function = (String, List[String])
+    /* node overlays */
 
     object Overlays
     {
       val empty = new Overlays(Multi_Map.empty)
     }
 
-    final class Overlays private(rep: Multi_Map[Command, Print_Function])
+    final class Overlays private(rep: Multi_Map[Command, (String, List[String])])
     {
       def commands: Set[Command] = rep.keySet
       def is_empty: Boolean = rep.isEmpty
-
-      def insert(cmd: Command, over: Print_Function): Overlays =
-        new Overlays(rep.insert(cmd, over))
-
-      def remove(cmd: Command, over: Print_Function): Overlays =
-        new Overlays(rep.remove(cmd, over))
-
-      def dest: List[(Command, Print_Function)] = rep.iterator.toList
+      def dest: List[(Command, (String, List[String]))] = rep.iterator.toList
+      def insert(cmd: Command, fn: String, args: List[String]): Overlays =
+        new Overlays(rep.insert(cmd, (fn, args)))
+      def remove(cmd: Command, fn: String, args: List[String]): Overlays =
+        new Overlays(rep.remove(cmd, (fn, args)))
     }
 
 

--- a/src/Pure/PIDE/editor.scala	Mon Aug 12 13:32:26 2013 +0200
+++ b/src/Pure/PIDE/editor.scala	Mon Aug 12 14:27:58 2013 +0200
@@ -16,5 +16,9 @@
   def current_snapshot(context: Context): Option[Document.Snapshot]
   def node_snapshot(name: Document.Node.Name): Document.Snapshot
   def current_command(context: Context, snapshot: Document.Snapshot): Option[(Command, Text.Offset)]
+
+  def node_overlays(name: Document.Node.Name): Document.Node.Overlays
+  def insert_overlay(command: Command, fn: String, args: List[String]): Unit
+  def remove_overlay(command: Command, fn: String, args: List[String]): Unit
 }
 

--- a/src/Tools/jEdit/src/document_model.scala	Mon Aug 12 13:32:26 2013 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Aug 12 14:27:58 2013 +0200
@@ -77,17 +77,6 @@
   }
 
 
-  /* overlays */
-
-  private var overlays = Document.Node.Overlays.empty
-
-  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 = overlays.remove(command, (name, args)) }
-
-
   /* perspective */
 
   // owned by Swing thread
@@ -115,7 +104,7 @@
         for {
           doc_view <- PIDE.document_views(buffer)
           range <- doc_view.perspective().ranges
-        } yield range), overlays)
+        } yield range), PIDE.editor.node_overlays(node_name))
     }
     else empty_perspective
   }

--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 13:32:26 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 14:27:58 2013 +0200
@@ -15,6 +15,8 @@
 
 class JEdit_Editor extends Editor[View]
 {
+  /* session */
+
   def session: Session = PIDE.session
 
   def flush()
@@ -34,6 +36,9 @@
     )
   }
 
+
+  /* current situation */
+
   def current_context: View =
     Swing_Thread.require { jEdit.getActiveView() }
 
@@ -72,4 +77,18 @@
       }
     }
   }
+
+
+  /* overlays */
+
+  private var overlays = Document.Overlays.empty
+
+  def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
+    synchronized { overlays(name) }
+
+  def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
+    synchronized { overlays = overlays.insert(command, fn, args) }
+
+  def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
+    synchronized { overlays = overlays.remove(command, fn, args) }
 }

--- a/src/Tools/jEdit/src/query_operation.scala	Mon Aug 12 13:32:26 2013 +0200
+++ b/src/Tools/jEdit/src/query_operation.scala	Mon Aug 12 14:27:58 2013 +0200
@@ -56,13 +56,8 @@
 
   private def remove_overlay()
   {
-    Swing_Thread.require()
-
-    for {
-      command <- current_location
-      buffer <- JEdit_Lib.jedit_buffer(command.node_name.node)
-      model <- PIDE.document_model(buffer)
-    } model.remove_overlay(command, operation_name, instance :: current_query)
+    current_location.foreach(command =>
+      editor.remove_overlay(command, operation_name, instance :: current_query))
   }
 
 
@@ -167,7 +162,7 @@
             current_location = Some(command)
             current_query = query
             current_status = Query_Operation.Status.WAITING
-            doc_view.model.insert_overlay(command, operation_name, instance :: query)
+            editor.insert_overlay(command, operation_name, instance :: query)
           case None =>
         }
         consume_status(current_status)