more uniform pending_input / pending_output;
explicit Document_Model.uri;
tuned;

--- a/src/Tools/VSCode/src/document_model.scala	Wed Dec 28 19:16:45 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Wed Dec 28 19:45:09 2016 +0100
@@ -20,10 +20,14 @@
   override def toString: String = node_name.toString
 
 
-  /* header */
+  /* name */
 
+  def uri: String = node_name.node
   def is_theory: Boolean = node_name.is_theory
 
+
+  /* header */
+
   def node_header(resources: VSCode_Resources): Document.Node.Header =
     resources.special_header(node_name) getOrElse
     {

--- a/src/Tools/VSCode/src/server.scala	Wed Dec 28 19:16:45 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Wed Dec 28 19:45:09 2016 +0100
@@ -89,6 +89,7 @@
   sealed case class State(
     session: Option[Session] = None,
     models: Map[String, Document_Model] = Map.empty,
+    pending_input: Set[Document.Node.Name] = Set.empty,
     pending_output: Set[Document.Node.Name] = Set.empty)
 }
 
@@ -121,11 +122,16 @@
     Standard_Thread.delay_last(options.seconds("vscode_input_delay")) {
       state.change(st =>
         {
-          val changed = (for { entry <- st.models.iterator if entry._2.changed } yield entry).toList
-          val edits = for { (_, model) <- changed; edit <- model.node_edits(resources) } yield edit
-          session.update(Document.Blobs.empty, edits)
+          val changed =
+            (for {
+              node_name <- st.pending_input.iterator
+              model <- st.models.get(node_name.node)
+              if model.changed } yield model).toList
+          session.update(Document.Blobs.empty,
+            for { model <- changed; edit <- model.node_edits(resources) } yield edit)
           st.copy(
-            models = (st.models /: changed)({ case (ms, (uri, m)) => ms + (uri -> m.unchanged) }))
+            models = (st.models /: changed) { case (ms, m) => ms + (m.uri -> m.unchanged) },
+            pending_input = Set.empty)
         })
     }
 
@@ -135,7 +141,9 @@
       {
         val node_name = resources.node_name(uri)
         val model = Document_Model(session, Line.Document(text, text_length), node_name)
-        st.copy(models = st.models + (uri -> model))
+        st.copy(
+          models = st.models + (uri -> model),
+          pending_input = st.pending_input + node_name)
       })
     delay_input.invoke()
   }
@@ -157,16 +165,15 @@
           val changed_iterator =
             for {
               node_name <- st.pending_output.iterator
-              uri = node_name.node
-              model <- st.models.get(uri)
+              model <- st.models.get(node_name.node)
               rendering = model.rendering(options)
               (diagnostics, model1) <- model.publish_diagnostics(rendering)
             } yield {
-              channel.diagnostics(uri, rendering.diagnostics_output(diagnostics))
-              (uri, model1)
+              channel.diagnostics(model1.uri, rendering.diagnostics_output(diagnostics))
+              model1
             }
           st.copy(
-            models = (st.models /: changed_iterator) { case (ms, (uri, m)) => ms + (uri -> m) },
+            models = (st.models /: changed_iterator) { case (ms, m) => ms + (m.uri -> m) },
             pending_output = Set.empty)
         })
     }