more uniform pending_input / pending_output;
authorwenzelm
Wed Dec 28 19:45:09 2016 +0100 (2016-12-28)
changeset 64690599873de8b01
parent 64689 f32efd2eeb2c
child 64691 db2b21a52f20
more uniform pending_input / pending_output;
explicit Document_Model.uri;
tuned;
src/Tools/VSCode/src/document_model.scala
src/Tools/VSCode/src/server.scala
     1.1 --- a/src/Tools/VSCode/src/document_model.scala	Wed Dec 28 19:16:45 2016 +0100
     1.2 +++ b/src/Tools/VSCode/src/document_model.scala	Wed Dec 28 19:45:09 2016 +0100
     1.3 @@ -20,10 +20,14 @@
     1.4    override def toString: String = node_name.toString
     1.5  
     1.6  
     1.7 -  /* header */
     1.8 +  /* name */
     1.9  
    1.10 +  def uri: String = node_name.node
    1.11    def is_theory: Boolean = node_name.is_theory
    1.12  
    1.13 +
    1.14 +  /* header */
    1.15 +
    1.16    def node_header(resources: VSCode_Resources): Document.Node.Header =
    1.17      resources.special_header(node_name) getOrElse
    1.18      {
     2.1 --- a/src/Tools/VSCode/src/server.scala	Wed Dec 28 19:16:45 2016 +0100
     2.2 +++ b/src/Tools/VSCode/src/server.scala	Wed Dec 28 19:45:09 2016 +0100
     2.3 @@ -89,6 +89,7 @@
     2.4    sealed case class State(
     2.5      session: Option[Session] = None,
     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  }
    2.10  
    2.11 @@ -121,11 +122,16 @@
    2.12      Standard_Thread.delay_last(options.seconds("vscode_input_delay")) {
    2.13        state.change(st =>
    2.14          {
    2.15 -          val changed = (for { entry <- st.models.iterator if entry._2.changed } yield entry).toList
    2.16 -          val edits = for { (_, model) <- changed; edit <- model.node_edits(resources) } yield edit
    2.17 -          session.update(Document.Blobs.empty, edits)
    2.18 +          val changed =
    2.19 +            (for {
    2.20 +              node_name <- st.pending_input.iterator
    2.21 +              model <- st.models.get(node_name.node)
    2.22 +              if model.changed } yield model).toList
    2.23 +          session.update(Document.Blobs.empty,
    2.24 +            for { model <- changed; edit <- model.node_edits(resources) } yield edit)
    2.25            st.copy(
    2.26 -            models = (st.models /: changed)({ case (ms, (uri, m)) => ms + (uri -> m.unchanged) }))
    2.27 +            models = (st.models /: changed) { case (ms, m) => ms + (m.uri -> m.unchanged) },
    2.28 +            pending_input = Set.empty)
    2.29          })
    2.30      }
    2.31  
    2.32 @@ -135,7 +141,9 @@
    2.33        {
    2.34          val node_name = resources.node_name(uri)
    2.35          val model = Document_Model(session, Line.Document(text, text_length), node_name)
    2.36 -        st.copy(models = st.models + (uri -> model))
    2.37 +        st.copy(
    2.38 +          models = st.models + (uri -> model),
    2.39 +          pending_input = st.pending_input + node_name)
    2.40        })
    2.41      delay_input.invoke()
    2.42    }
    2.43 @@ -157,16 +165,15 @@
    2.44            val changed_iterator =
    2.45              for {
    2.46                node_name <- st.pending_output.iterator
    2.47 -              uri = node_name.node
    2.48 -              model <- st.models.get(uri)
    2.49 +              model <- st.models.get(node_name.node)
    2.50                rendering = model.rendering(options)
    2.51                (diagnostics, model1) <- model.publish_diagnostics(rendering)
    2.52              } yield {
    2.53 -              channel.diagnostics(uri, rendering.diagnostics_output(diagnostics))
    2.54 -              (uri, model1)
    2.55 +              channel.diagnostics(model1.uri, rendering.diagnostics_output(diagnostics))
    2.56 +              model1
    2.57              }
    2.58            st.copy(
    2.59 -            models = (st.models /: changed_iterator) { case (ms, (uri, m)) => ms + (uri -> m) },
    2.60 +            models = (st.models /: changed_iterator) { case (ms, m) => ms + (m.uri -> m) },
    2.61              pending_output = Set.empty)
    2.62          })
    2.63      }