1.1 --- a/src/Tools/VSCode/src/server.scala	Wed Dec 28 19:16:45 2016 +0100
     1.2 +++ b/src/Tools/VSCode/src/server.scala	Wed Dec 28 19:45:09 2016 +0100
     1.3 @@ -89,6 +89,7 @@
     1.4    sealed case class State(
     1.5      session: Option[Session] = None,
     1.6      models: Map[String, Document_Model] = Map.empty,
     1.7 +    pending_input: Set[Document.Node.Name] = Set.empty,
     1.8      pending_output: Set[Document.Node.Name] = Set.empty)
     1.9  }
    1.10  
    1.11 @@ -121,11 +122,16 @@
    1.12      Standard_Thread.delay_last(options.seconds("vscode_input_delay")) {
    1.13        state.change(st =>
    1.14          {
    1.15 -          val changed = (for { entry <- st.models.iterator if entry._2.changed } yield entry).toList
    1.16 -          val edits = for { (_, model) <- changed; edit <- model.node_edits(resources) } yield edit
    1.17 -          session.update(Document.Blobs.empty, edits)
    1.18 +          val changed =
    1.19 +            (for {
    1.20 +              node_name <- st.pending_input.iterator
    1.21 +              model <- st.models.get(node_name.node)
    1.22 +              if model.changed } yield model).toList
    1.23 +          session.update(Document.Blobs.empty,
    1.24 +            for { model <- changed; edit <- model.node_edits(resources) } yield edit)
    1.25            st.copy(
    1.26 -            models = (st.models /: changed)({ case (ms, (uri, m)) => ms + (uri -> m.unchanged) }))
    1.27 +            models = (st.models /: changed) { case (ms, m) => ms + (m.uri -> m.unchanged) },
    1.28 +            pending_input = Set.empty)
    1.29          })
    1.30      }
    1.31  
    1.32 @@ -135,7 +141,9 @@
    1.33        {
    1.34          val node_name = resources.node_name(uri)
    1.35          val model = Document_Model(session, Line.Document(text, text_length), node_name)
    1.36 -        st.copy(models = st.models + (uri -> model))
    1.37 +        st.copy(
    1.38 +          models = st.models + (uri -> model),
    1.39 +          pending_input = st.pending_input + node_name)
    1.40        })
    1.41      delay_input.invoke()
    1.42    }
    1.43 @@ -157,16 +165,15 @@
    1.44            val changed_iterator =
    1.45              for {
    1.46                node_name <- st.pending_output.iterator
    1.47 -              uri = node_name.node
    1.48 -              model <- st.models.get(uri)
    1.49 +              model <- st.models.get(node_name.node)
    1.50                rendering = model.rendering(options)
    1.51                (diagnostics, model1) <- model.publish_diagnostics(rendering)
    1.52              } yield {
    1.53 -              channel.diagnostics(uri, rendering.diagnostics_output(diagnostics))
    1.54 -              (uri, model1)
    1.55 +              channel.diagnostics(model1.uri, rendering.diagnostics_output(diagnostics))
    1.56 +              model1
    1.57              }
    1.58            st.copy(
    1.59 -            models = (st.models /: changed_iterator) { case (ms, (uri, m)) => ms + (uri -> m) },
    1.60 +            models = (st.models /: changed_iterator) { case (ms, m) => ms + (m.uri -> m) },
    1.61              pending_output = Set.empty)
    1.62          })
    1.63      }