# HG changeset patch
# User paulson
# Date 1739707061 0
# Node ID fa2c960fb232baf56e9590c4edc000a8cc55acab
# Parent  207f2120cc9298f32b49126576f467c2aee3e532# Parent  cddce3a4ef84a90b0cd4ac16a804e945042b8805
merged

diff -r cddce3a4ef84 -r fa2c960fb232 src/Tools/VSCode/src/pretty_text_panel.scala
--- a/src/Tools/VSCode/src/pretty_text_panel.scala	Sun Feb 16 11:57:33 2025 +0000
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala	Sun Feb 16 11:57:41 2025 +0000
@@ -40,53 +40,53 @@
     val formatted =
       Pretty.formatted(Pretty.separate(output), margin = margin, metric = Symbol.Metric)
 
-    if (formatted == current_formatted) return
-
-    current_output = output
-    current_formatted = formatted
+    if (formatted != current_formatted) {
+      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)
-              source <- resources.source_file(thy_file)
-              uri = File.uri(Path.explode(source).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 {
-      def convert_symbols(body: XML.Body): XML.Body = {
-        body.map {
-          case XML.Elem(markup, body) => XML.Elem(markup, convert_symbols(body))
-          case XML.Text(content) => XML.Text(resources.output_text(content))
-        }
+      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)
+                source <- resources.source_file(thy_file)
+                uri = File.uri(Path.explode(source).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)
       }
-
-      val converted = convert_symbols(formatted)
+      else {
+        def convert_symbols(body: XML.Body): XML.Body =
+          body.map {
+            case XML.Elem(markup, body) => XML.Elem(markup, convert_symbols(body))
+            case XML.Text(content) => XML.Text(resources.output_text(content))
+          }
 
-      val tree = Markup_Tree.from_XML(converted)
-      val text = XML.content(converted)
+        val converted = convert_symbols(formatted)
+
+        val tree = Markup_Tree.from_XML(converted)
+        val text = XML.content(converted)
 
-      val document = Line.Document(text)
-      val decorations =
-        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
+        val document = Line.Document(text)
+        val decorations =
+          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(text, Some(LSP.Decoration(decorations))))
+        channel.write(output_json(text, Some(LSP.Decoration(decorations))))
+      }
     }
   }
 }