src/Tools/VSCode/src/vscode_resources.scala
changeset 64704 08c2d80428ff
parent 64703 a115391494ed
child 64706 3ebf9f8299df
equal deleted inserted replaced
64703:a115391494ed 64704:08c2d80428ff
    99       {
    99       {
   100         val changed_iterator =
   100         val changed_iterator =
   101           for {
   101           for {
   102             node_name <- st.pending_output.iterator
   102             node_name <- st.pending_output.iterator
   103             model <- st.models.get(node_name.node)
   103             model <- st.models.get(node_name.node)
   104             rendering = model.rendering(options)
   104             rendering = model.rendering()
   105             (diagnostics, model1) <- model.publish_diagnostics(rendering)
   105             (diagnostics, model1) <- model.publish_diagnostics(rendering)
   106           } yield {
   106           } yield {
   107             channel.diagnostics(model1.uri, rendering.diagnostics_output(diagnostics))
   107             channel.diagnostics(model1.uri, rendering.diagnostics_output(diagnostics))
   108             model1
   108             model1
   109           }
   109           }