# HG changeset patch # User wenzelm # Date 1482951535 -3600 # Node ID db2b21a52f202358fb87d5de9c62cb3d954fcb4b # Parent 599873de8b012944c710bbb3371a9f0141c85ae0 prefer stable state -- reduce repeated diagnostics; diff -r 599873de8b01 -r db2b21a52f20 src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Wed Dec 28 19:45:09 2016 +0100 +++ b/src/Tools/VSCode/src/server.scala Wed Dec 28 19:58:55 2016 +0100 @@ -158,24 +158,28 @@ delay_output.invoke() } - private val delay_output = + private val delay_output: Standard_Thread.Delay = Standard_Thread.delay_last(options.seconds("vscode_output_delay")) { - state.change(st => - { - val changed_iterator = - for { - node_name <- st.pending_output.iterator - model <- st.models.get(node_name.node) - rendering = model.rendering(options) - (diagnostics, model1) <- model.publish_diagnostics(rendering) - } yield { - channel.diagnostics(model1.uri, rendering.diagnostics_output(diagnostics)) - model1 - } - st.copy( - models = (st.models /: changed_iterator) { case (ms, m) => ms + (m.uri -> m) }, - pending_output = Set.empty) - }) + if (session.current_state().stable_tip_version.isEmpty) delay_output.invoke() + else { + state.change(st => + { + val changed_iterator = + for { + node_name <- st.pending_output.iterator + model <- st.models.get(node_name.node) + rendering = model.rendering(options) + (diagnostics, model1) <- model.publish_diagnostics(rendering) + } yield { + channel.diagnostics(model1.uri, rendering.diagnostics_output(diagnostics)) + model1 + } + st.copy( + models = (st.models /: changed_iterator) { case (ms, m) => ms + (m.uri -> m) }, + pending_output = Set.empty) + } + ) + } }