1.1 --- a/src/Tools/VSCode/src/server.scala	Fri Dec 30 11:46:34 2016 +0100
     1.2 +++ b/src/Tools/VSCode/src/server.scala	Fri Dec 30 11:54:11 2016 +0100
     1.3 @@ -125,7 +125,7 @@
     1.4    private val commands_changed =
     1.5      Session.Consumer[Session.Commands_Changed](getClass.getName) {
     1.6        case changed if changed.nodes.nonEmpty =>
     1.7 -        resources.update_output(changed.nodes)
     1.8 +        resources.update_output(changed.nodes.toList.map(_.node))
     1.9          delay_output.invoke()
    1.10        case _ =>
    1.11      }

     2.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 30 11:46:34 2016 +0100
     2.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 30 11:54:11 2016 +0100
     2.3 @@ -29,8 +29,8 @@
     2.4  
     2.5    sealed case class State(
     2.6      models: Map[String, Document_Model] = Map.empty,
     2.7 -    pending_input: Set[Document.Node.Name] = Set.empty,
     2.8 -    pending_output: Set[Document.Node.Name] = Set.empty)
     2.9 +    pending_input: Set[String] = Set.empty,
    2.10 +    pending_output: Set[String] = Set.empty)
    2.11  }
    2.12  
    2.13  class VSCode_Resources(
    2.14 @@ -64,8 +64,8 @@
    2.15    {
    2.16      state.change(st =>
    2.17        st.copy(
    2.18 -        models = st.models + (model.node_name.node -> model),
    2.19 -        pending_input = st.pending_input + model.node_name))
    2.20 +        models = st.models + (model.uri -> model),
    2.21 +        pending_input = st.pending_input + model.uri))
    2.22    }
    2.23  
    2.24  
    2.25 @@ -77,8 +77,8 @@
    2.26        {
    2.27          val changed =
    2.28            (for {
    2.29 -            node_name <- st.pending_input.iterator
    2.30 -            model <- st.models.get(node_name.node)
    2.31 +            uri <- st.pending_input.iterator
    2.32 +            model <- st.models.get(uri)
    2.33              res <- model.flush_edits
    2.34            } yield res).toList
    2.35  
    2.36 @@ -92,7 +92,7 @@
    2.37  
    2.38    /* pending output */
    2.39  
    2.40 -  def update_output(changed_nodes: Set[Document.Node.Name]): Unit =
    2.41 +  def update_output(changed_nodes: List[String]): Unit =
    2.42      state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
    2.43  
    2.44    def flush_output(channel: Channel)
    2.45 @@ -101,8 +101,8 @@
    2.46        {
    2.47          val changed_iterator =
    2.48            for {
    2.49 -            node_name <- st.pending_output.iterator
    2.50 -            model <- st.models.get(node_name.node)
    2.51 +            uri <- st.pending_output.iterator
    2.52 +            model <- st.models.get(uri)
    2.53              rendering = model.rendering()
    2.54              (diagnostics, model1) <- model.publish_diagnostics(rendering)
    2.55            } yield {