lsp: added Pretty_Text_Panel module;

--- a/etc/build.props	Wed Jun 12 21:26:31 2024 +0200
+++ b/etc/build.props	Fri Jun 14 10:21:03 2024 +0200
@@ -262,6 +262,7 @@
   src/Tools/VSCode/src/dynamic_output.scala \
   src/Tools/VSCode/src/language_server.scala \
   src/Tools/VSCode/src/lsp.scala \
+  src/Tools/VSCode/src/pretty_text_panel.scala \
   src/Tools/VSCode/src/preview_panel.scala \
   src/Tools/VSCode/src/state_panel.scala \
   src/Tools/VSCode/src/vscode_main.scala \

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala	Fri Jun 14 10:21:03 2024 +0200
@@ -0,0 +1,85 @@
+/*  Title:      Tools/VSCode/src/pretty_text_panel.scala
+    Author:     Thomas Lindae, TU Muenchen
+
+Pretty-printed text or HTML with decorations.
+*/
+
+package isabelle.vscode
+
+import isabelle._
+
+object Pretty_Text_Panel {
+  def apply(
+    resources: VSCode_Resources,
+    channel: Channel,
+    output: (String, Option[LSP.Decoration_List]) => Unit
+  ): Pretty_Text_Panel = new Pretty_Text_Panel(resources, channel, output)
+}
+
+class Pretty_Text_Panel private(
+  resources: VSCode_Resources,
+  channel: Channel,
+  output: (String, Option[LSP.Decoration_List]) => Unit
+) {
+  private var current_body: XML.Body = Nil
+  private var current_formatted: XML.Body = Nil
+  private var margin: Double = resources.message_margin
+
+  private val delay_margin = Delay.last(resources.output_delay, channel.Error_Logger) {
+    refresh(current_body)
+  }
+  
+  def update_margin(new_margin: Double): Unit = {
+    margin = new_margin
+    delay_margin.invoke()
+  }
+
+  def refresh(body: XML.Body): Unit = {
+    val formatted = Pretty.formatted(Pretty.separate(body), margin = margin, metric = Symbol.Metric)
+
+    if (formatted == current_formatted) return
+
+    current_body = body
+    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)
+      output(HTML.source(html).toString, None)
+    } 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(Symbol.output(resources.unicode_symbols, content))
+        }
+      }
+
+      val tree = Markup_Tree.from_XML(convert_symbols(formatted))
+      val text = resources.output_text(XML.content(formatted))
+
+      val document = Line.Document(text)
+      val decorations = tree
+        .cumulate(Text.Range.full, None: Option[String], Rendering.text_color_elements, (_, m) => {
+          Some(Some(m.info.name))
+        })
+        .flatMap(e => e._2 match {
+          case None => None
+          case Some(i) => Some((document.range(e._1), "text_" ++ Rendering.text_color(i).toString))
+        })
+        .groupMap(_._2)(e => LSP.Decoration_Options(e._1, List())).toList
+
+      output(text, Some(decorations))
+    }
+  }
+}
+