lsp: added State and Dynamic Output html_output and margin handling;
authorThomas Lindae <thomas.lindae@in.tum.de>
Wed, 01 May 2024 12:34:53 +0200
changeset 81025 d4eb94b46e83
parent 81024 d1535ba3b1ca
child 81026 c4bc259393f6
lsp: added State and Dynamic Output html_output and margin handling;
src/Tools/VSCode/src/dynamic_output.scala
src/Tools/VSCode/src/state_panel.scala
src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/dynamic_output.scala	Wed May 01 12:30:53 2024 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Wed May 01 12:34:53 2024 +0200
@@ -15,7 +15,9 @@
     def handle_update(
       resources: VSCode_Resources,
       channel: Channel,
-      restriction: Option[Set[Command]]
+      restriction: Option[Set[Command]],
+      html_output: Boolean,
+      margin: Double,
     ): State = {
       val st1 =
         resources.get_caret() match {
@@ -36,19 +38,25 @@
             else this
         }
       if (st1.output != 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, Pretty.separate(st1.output))
-        channel.write(LSP.Dynamic_Output(HTML.source(html).toString))
+        if (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 separate = Pretty.separate(st1.output)
+          val formatted = Pretty.formatted(separate, margin = margin)
+          val html = node_context.make_html(elements, formatted)
+          channel.write(LSP.Dynamic_Output(HTML.source(html).toString))
+        } else {
+          channel.write(LSP.Dynamic_Output(resources.output_pretty(st1.output, margin = margin)))
+        }
       }
       st1
     }
@@ -60,9 +68,12 @@
 
 class Dynamic_Output private(server: Language_Server) {
   private val state = Synchronized(Dynamic_Output.State())
+  private val margin: Double = 80
 
-  private def handle_update(restriction: Option[Set[Command]]): Unit =
-    state.change(_.handle_update(server.resources, server.channel, restriction))
+  private def handle_update(restriction: Option[Set[Command]]): Unit = {
+    val html_output = server.resources.html_output
+    state.change(_.handle_update(server.resources, server.channel, restriction, html_output, margin))
+  }
 
 
   /* main */
--- a/src/Tools/VSCode/src/state_panel.scala	Wed May 01 12:30:53 2024 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala	Wed May 01 12:34:53 2024 +0200
@@ -47,6 +47,7 @@
   /* output */
 
   val id: Counter.ID = State_Panel.make_id()
+  private val margin: Double = 80
 
   private def output(content: String): Unit =
     server.channel.write(LSP.State_Output(id, content, auto_update_enabled.value))
@@ -63,19 +64,25 @@
     new Query_Operation(server.editor, (), "print_state", _ => (),
       (_, _, body) =>
         if (output_active.value && body.nonEmpty) {
-          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 <- server.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, Pretty.separate(body))
-          output(HTML.source(html).toString)
+          if (server.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 <- server.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 separate = Pretty.separate(body)
+            val formatted = Pretty.formatted(separate, margin = margin)
+            val html = node_context.make_html(elements, formatted)
+            output(HTML.source(html).toString)
+          } else {
+            output(server.resources.output_pretty(body, margin))
+          }
         })
 
   def locate(): Unit = print_state.locate_query()
--- a/src/Tools/VSCode/src/vscode_resources.scala	Wed May 01 12:30:53 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed May 01 12:34:53 2024 +0200
@@ -337,7 +337,7 @@
   def output_xml(xml: XML.Tree): String =
     output_text(XML.content(xml))
 
-  def output_pretty(body: XML.Body, margin: Int): String =
+  def output_pretty(body: XML.Body, margin: Double): String =
     output_text(Pretty.string_of(body, margin = margin, metric = Symbol.Metric))
   def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin)
   def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin)