maintain overlays within main state of document models;
proper pending_input for Isabelle/VSCode;

--- a/src/Pure/PIDE/editor.scala	Fri Jun 16 22:40:05 2017 +0200
+++ b/src/Pure/PIDE/editor.scala	Sat Jun 17 14:47:36 2017 +0200
@@ -14,6 +14,10 @@
   def session: Session
   def flush(): Unit
   def invoke(): Unit
+
+
+  /* current situation */
+
   def current_node(context: Context): Option[Document.Node.Name]
   def current_node_snapshot(context: Context): Option[Document.Snapshot]
   def node_snapshot(name: Document.Node.Name): Document.Snapshot
@@ -22,16 +26,9 @@
 
   /* overlays */
 
-  private val overlays = Synchronized(Document.Overlays.empty)
-
-  def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
-    overlays.value(name)
-
-  def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
-    overlays.change(_.insert(command, fn, args))
-
-  def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
-    overlays.change(_.remove(command, fn, args))
+  def node_overlays(name: Document.Node.Name): Document.Node.Overlays
+  def insert_overlay(command: Command, fn: String, args: List[String])
+  def remove_overlay(command: Command, fn: String, args: List[String])
 
 
   /* hyperlinks */

--- a/src/Tools/VSCode/src/server.scala	Fri Jun 16 22:40:05 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala	Sat Jun 17 14:47:36 2017 +0200
@@ -436,10 +436,15 @@
 
   object editor extends Server.Editor
   {
+    /* session */
+
     override def session: Session = server.session
     override def flush(): Unit = resources.flush_input(session)
     override def invoke(): Unit = delay_input.invoke()
 
+
+    /* current situation */
+
     override def current_node(context: Unit): Option[Document.Node.Name] =
       resources.get_caret().map(_.model.node_name)
     override def current_node_snapshot(context: Unit): Option[Document.Snapshot] =
@@ -463,10 +468,28 @@
     override def current_command(context: Unit, snapshot: Document.Snapshot): Option[Command] =
       current_command(snapshot)
 
+
+    /* overlays */
+
+    override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
+      resources.node_overlays(name)
+
+    override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
+      resources.insert_overlay(command, fn, args)
+
+    override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
+      resources.remove_overlay(command, fn, args)
+
+
+    /* hyperlinks */
+
     override def hyperlink_command(
       focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
         : Option[Hyperlink] = None
 
+
+    /* dispatcher thread */
+
     override def assert_dispatcher[A](body: => A): A = session.assert_dispatcher(body)
     override def require_dispatcher[A](body: => A): A = session.require_dispatcher(body)
     override def send_dispatcher(body: => Unit): Unit = session.send_dispatcher(body)

--- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Jun 16 22:40:05 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sat Jun 17 14:47:36 2017 +0200
@@ -21,6 +21,7 @@
   sealed case class State(
     models: Map[JFile, Document_Model] = Map.empty,
     caret: Option[(JFile, Line.Position)] = None,
+    overlays: Document.Overlays = Document.Overlays.empty,
     pending_input: Set[JFile] = Set.empty,
     pending_output: Set[JFile] = Set.empty)
   {
@@ -49,6 +50,14 @@
           (_, model) <- models.iterator
           blob <- model.get_blob
         } yield (model.node_name -> blob)).toMap)
+
+    def change_overlay(insert: Boolean, file: JFile,
+        command: Command, fn: String, args: List[String]): State =
+      copy(
+        overlays =
+          if (insert) overlays.insert(command, fn, args)
+          else overlays.remove(command, fn, args),
+        pending_input = pending_input + file)
   }
 
 
@@ -183,6 +192,18 @@
       })
 
 
+  /* overlays */
+
+  def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
+    state.value.overlays(name)
+
+  def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
+    state.change(_.change_overlay(true, node_file(command.node_name), command, fn, args))
+
+  def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
+    state.change(_.change_overlay(false, node_file(command.node_name), command, fn, args))
+
+
   /* resolve dependencies */
 
   def resolve_dependencies(

--- a/src/Tools/jEdit/src/document_model.scala	Fri Jun 16 22:40:05 2017 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Sat Jun 17 14:47:36 2017 +0200
@@ -27,7 +27,8 @@
 
   sealed case class State(
     models: Map[Document.Node.Name, Document_Model] = Map.empty,
-    buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty)
+    buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty,
+    overlays: Document.Overlays = Document.Overlays.empty)
   {
     def file_models_iterator: Iterator[(Document.Node.Name, File_Model)] =
       for {
@@ -83,6 +84,18 @@
     } yield info.map((_, model))
 
 
+  /* overlays */
+
+  def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
+    state.value.overlays(name)
+
+  def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
+    state.change(st => st.copy(overlays = st.overlays.insert(command, fn, args)))
+
+  def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
+    state.change(st => st.copy(overlays = st.overlays.remove(command, fn, args)))
+
+
   /* sync external files */
 
   def sync_files(changed_files: Set[JFile]): Boolean =

--- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Jun 16 22:40:05 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Sat Jun 17 14:47:36 2017 +0200
@@ -83,6 +83,18 @@
   }
 
 
+  /* overlays */
+
+  override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
+    Document_Model.node_overlays(name)
+
+  override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
+    Document_Model.insert_overlay(command, fn, args)
+
+  override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
+    Document_Model.remove_overlay(command, fn, args)
+
+
   /* navigation */
 
   def push_position(view: View)