lsp: converted dynamic output to use a pretty text panel;

--- a/src/Tools/VSCode/src/dynamic_output.scala	Fri Jun 14 10:21:03 2024 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Fri Jun 14 10:21:28 2024 +0200
@@ -11,56 +11,33 @@
 
 
 object Dynamic_Output {
-  sealed case class State(do_update: Boolean = true, output: List[XML.Tree] = Nil) {
-    def handle_update(
-      resources: VSCode_Resources,
-      channel: Channel,
-      restriction: Option[Set[Command]],
-      margin: Double,
-      force: Boolean,
-    ): State = {
-      val st1 =
-        resources.get_caret() match {
-          case None => copy(output = Nil)
-          case Some(caret) =>
-            val snapshot = resources.snapshot(caret.model)
-            if (do_update && !snapshot.is_outdated) {
-              snapshot.current_command(caret.node_name, caret.offset) match {
-                case None => copy(output = Nil)
-                case Some(command) =>
-                  copy(output =
-                    if (restriction.isEmpty || restriction.get.contains(command)) {
-                      val output_state = resources.options.bool("editor_output_state")
-                      Rendering.output_messages(snapshot.command_results(command), output_state)
-                    } else output)
-              }
-            }
-            else this
-        }
-      if (st1.output != output || force) {
-        val (output, decorations) = resources.output_pretty_panel(st1.output, margin)
-        channel.write(LSP.Dynamic_Output(output, decorations))
-      }
-      st1
-    }
-  }
-
   def apply(server: Language_Server): Dynamic_Output = new Dynamic_Output(server)
 }
 
-
 class Dynamic_Output private(server: Language_Server) {
-  private val state = Synchronized(Dynamic_Output.State())
-  private val margin_ = Synchronized(None: Option[Double])
-  def margin: Double = margin_.value.getOrElse(server.resources.message_margin)
-
-  private val delay_margin = Delay.last(server.resources.output_delay, server.channel.Error_Logger) {
-    handle_update(None, force = true)
-  }
+  private val pretty_panel_ = Synchronized(None: Option[Pretty_Text_Panel])
+  def pretty_panel: Pretty_Text_Panel = pretty_panel_.value.getOrElse(error("No Pretty Panel for Dynamic Output"))
 
   private def handle_update(restriction: Option[Set[Command]], force: Boolean = false): Unit = {
-    state.change(
-      _.handle_update(server.resources, server.channel, restriction, margin, force))
+    val output =
+      server.resources.get_caret() match {
+        case None => Some(Nil)
+        case Some(caret) =>
+          val snapshot = server.resources.snapshot(caret.model)
+          snapshot.current_command(caret.node_name, caret.offset) match {
+            case None => Some(Nil)
+            case Some(command) =>
+              if (restriction.isEmpty || restriction.get.contains(command)) {
+                val output_state = server.resources.options.bool("editor_output_state")
+                Some(Rendering.output_messages(snapshot.command_results(command), output_state))
+              } else None
+          }
+      }
+      
+    output match {
+      case None =>
+      case Some(output) => pretty_panel.refresh(output)
+    }
   }
 
 
@@ -78,6 +55,11 @@
   def init(): Unit = {
     server.session.commands_changed += main
     server.session.caret_focus += main
+    pretty_panel_.change(p => Some(Pretty_Text_Panel(
+      server.resources,
+      server.channel,
+      (output_text, decorations) => { server.channel.write(LSP.Dynamic_Output(output_text, decorations)) }
+    )))
     handle_update(None)
   }
 
@@ -87,7 +69,6 @@
   }
 
   def set_margin(margin: Double): Unit = {
-    margin_.change(_ => Some(margin))
-    delay_margin.invoke()
+    pretty_panel.update_margin(margin)
   }
 }