# HG changeset patch
# User wenzelm
# Date 1754490456 -7200
# Node ID adaea1a92086bfadf3ad419d4ca2ed7516e4b4dc
# Parent  e879d01bcf451ed85a26e5dfcd995b5760810d53
more robust: commit state only after publishing message;

diff -r e879d01bcf45 -r adaea1a92086 src/Tools/VSCode/src/pretty_text_panel.scala
--- a/src/Tools/VSCode/src/pretty_text_panel.scala	Wed Aug 06 16:17:12 2025 +0200
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala	Wed Aug 06 16:27:36 2025 +0200
@@ -43,45 +43,46 @@
       Pretty.formatted(Pretty.separate(output), margin = margin, metric = Symbol.Metric)
 
     if (formatted != current_formatted) {
+      val message = {
+        if (resources.html_output) {
+          val node_context =
+            new Browser_Info.Node_Context {
+              override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] =
+                for {
+                  thy_file <- Position.Def_File.unapply(props)
+                  def_line <- Position.Def_Line.unapply(props)
+                  platform_path <- session.store.source_file(thy_file)
+                  uri = File.uri(Path.explode(File.standard_path(platform_path)).absolute_file)
+                } yield HTML.link(uri.toString + "#" + def_line, body)
+            }
+          val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full)
+          val html = node_context.make_html(elements, formatted)
+          output_json(HTML.source(html).toString, None)
+        }
+        else {
+          val converted = resources.output_text_xml(formatted)
+          val converted_tree = Markup_Tree.from_XML(converted)
+          val converted_text = XML.content(converted)
+
+          val document = Line.Document(converted_text)
+          val decorations =
+            converted_tree.cumulate[Option[Markup]](Text.Range.full, None, Rendering.text_color_elements,
+              { case (_, m) => Some(Some(m.info.markup)) }
+            ).flatMap(info =>
+                info.info match {
+                  case Some(markup) =>
+                    val range = document.range(info.range)
+                    Some((range, "text_" + Rendering.get_text_color(markup).get.toString))
+                  case None => None
+                }
+            ).groupMap(_._2)(e => LSP.Decoration_Options(e._1, Nil)).toList
+
+          output_json(converted_text, Some(LSP.Decoration(decorations)))
+        }
+      }
+      channel.write(message)
       current_output = output
       current_formatted = formatted
-
-      if (resources.html_output) {
-        val node_context =
-          new Browser_Info.Node_Context {
-            override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] =
-              for {
-                thy_file <- Position.Def_File.unapply(props)
-                def_line <- Position.Def_Line.unapply(props)
-                platform_path <- session.store.source_file(thy_file)
-                uri = File.uri(Path.explode(File.standard_path(platform_path)).absolute_file)
-              } yield HTML.link(uri.toString + "#" + def_line, body)
-          }
-        val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full)
-        val html = node_context.make_html(elements, formatted)
-        val message = output_json(HTML.source(html).toString, None)
-        channel.write(message)
-      }
-      else {
-        val converted = resources.output_text_xml(formatted)
-        val converted_tree = Markup_Tree.from_XML(converted)
-        val converted_text = XML.content(converted)
-
-        val document = Line.Document(converted_text)
-        val decorations =
-          converted_tree.cumulate[Option[Markup]](Text.Range.full, None, Rendering.text_color_elements,
-            { case (_, m) => Some(Some(m.info.markup)) }
-          ).flatMap(info =>
-              info.info match {
-                case Some(markup) =>
-                  val range = document.range(info.range)
-                  Some((range, "text_" + Rendering.get_text_color(markup).get.toString))
-                case None => None
-              }
-          ).groupMap(_._2)(e => LSP.Decoration_Options(e._1, Nil)).toList
-
-        channel.write(output_json(converted_text, Some(LSP.Decoration(decorations))))
-      }
     }
   }
 }