src/Tools/VSCode/src/server.scala
changeset 64691 db2b21a52f20
parent 64690 599873de8b01
child 64692 ccf017e2f2b4
     1.1 --- a/src/Tools/VSCode/src/server.scala	Wed Dec 28 19:45:09 2016 +0100
     1.2 +++ b/src/Tools/VSCode/src/server.scala	Wed Dec 28 19:58:55 2016 +0100
     1.3 @@ -158,24 +158,28 @@
     1.4          delay_output.invoke()
     1.5      }
     1.6  
     1.7 -  private val delay_output =
     1.8 +  private val delay_output: Standard_Thread.Delay =
     1.9      Standard_Thread.delay_last(options.seconds("vscode_output_delay")) {
    1.10 -      state.change(st =>
    1.11 -        {
    1.12 -          val changed_iterator =
    1.13 -            for {
    1.14 -              node_name <- st.pending_output.iterator
    1.15 -              model <- st.models.get(node_name.node)
    1.16 -              rendering = model.rendering(options)
    1.17 -              (diagnostics, model1) <- model.publish_diagnostics(rendering)
    1.18 -            } yield {
    1.19 -              channel.diagnostics(model1.uri, rendering.diagnostics_output(diagnostics))
    1.20 -              model1
    1.21 -            }
    1.22 -          st.copy(
    1.23 -            models = (st.models /: changed_iterator) { case (ms, m) => ms + (m.uri -> m) },
    1.24 -            pending_output = Set.empty)
    1.25 -        })
    1.26 +      if (session.current_state().stable_tip_version.isEmpty) delay_output.invoke()
    1.27 +      else {
    1.28 +        state.change(st =>
    1.29 +          {
    1.30 +            val changed_iterator =
    1.31 +              for {
    1.32 +                node_name <- st.pending_output.iterator
    1.33 +                model <- st.models.get(node_name.node)
    1.34 +                rendering = model.rendering(options)
    1.35 +                (diagnostics, model1) <- model.publish_diagnostics(rendering)
    1.36 +              } yield {
    1.37 +                channel.diagnostics(model1.uri, rendering.diagnostics_output(diagnostics))
    1.38 +                model1
    1.39 +              }
    1.40 +            st.copy(
    1.41 +              models = (st.models /: changed_iterator) { case (ms, m) => ms + (m.uri -> m) },
    1.42 +              pending_output = Set.empty)
    1.43 +          }
    1.44 +        )
    1.45 +      }
    1.46      }
    1.47  
    1.48