--- a/src/Tools/VSCode/src/dynamic_output.scala Wed Jun 12 20:54:11 2024 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala Wed Jun 12 21:22:01 2024 +0200
@@ -16,7 +16,6 @@
resources: VSCode_Resources,
channel: Channel,
restriction: Option[Set[Command]],
- html_output: Boolean,
margin: Double,
force: Boolean,
): State = {
@@ -39,26 +38,8 @@
else this
}
if (st1.output != output || force) {
- 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 {
- val (output, decorations) = resources.output_pretty_with_decorations(st1.output, margin)
- channel.write(LSP.Dynamic_Output(output, Some(decorations)))
- }
+ val (output, decorations) = resources.output_pretty_panel(st1.output, margin)
+ channel.write(LSP.Dynamic_Output(output, decorations))
}
st1
}
@@ -78,9 +59,8 @@
}
private def handle_update(restriction: Option[Set[Command]], force: Boolean = false): Unit = {
- val html_output = server.resources.html_output
state.change(
- _.handle_update(server.resources, server.channel, restriction, html_output, margin, force))
+ _.handle_update(server.resources, server.channel, restriction, margin, force))
}
--- a/src/Tools/VSCode/src/lsp.scala Wed Jun 12 20:54:11 2024 +0200
+++ b/src/Tools/VSCode/src/lsp.scala Wed Jun 12 21:22:01 2024 +0200
@@ -478,7 +478,9 @@
JSON.optional("hover_message" -> MarkedStrings.json(hover_message))
}
- sealed case class Decoration(decorations: List[(String, List[Decoration_Options])]) {
+ type Decoration_List = List[(String, List[Decoration_Options])]
+
+ sealed case class Decoration(decorations: Decoration_List) {
def json(file: JFile): JSON.T =
Notification("PIDE/decoration",
JSON.Object(
@@ -532,7 +534,7 @@
/* dynamic output */
object Dynamic_Output {
- def apply(content: String, decorations: Option[List[(String, List[Decoration_Options])]] = None): JSON.T =
+ def apply(content: String, decorations: Option[Decoration_List] = None): JSON.T =
Notification("PIDE/dynamic_output",
JSON.Object("content" -> content) ++
JSON.optional(
@@ -561,7 +563,7 @@
id: Counter.ID,
content: String,
auto_update: Boolean,
- decorations: Option[List[(String, List[Decoration_Options])]] = None
+ decorations: Option[Decoration_List] = None
): JSON.T =
Notification("PIDE/state_output",
JSON.Object("id" -> id, "content" -> content, "auto_update" -> auto_update) ++
--- a/src/Tools/VSCode/src/state_panel.scala Wed Jun 12 20:54:11 2024 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala Wed Jun 12 21:22:01 2024 +0200
@@ -59,9 +59,7 @@
server.editor.send_dispatcher(update(force = true))
}
- private def output(
- content: String,
- decorations: Option[List[(String, List[LSP.Decoration_Options])]] = None): Unit =
+ private def output(content: String, decorations: Option[LSP.Decoration_List] = None): Unit =
server.channel.write(LSP.State_Output(id, content, auto_update_enabled.value, decorations))
private def init_response(id: LSP.Id): Unit =
@@ -76,26 +74,8 @@
new Query_Operation(server.editor, (), "print_state", _ => (),
(_, _, body) =>
if (output_active.value && body.nonEmpty) {
- 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.value)
- val html = node_context.make_html(elements, formatted)
- output(HTML.source(html).toString)
- } else {
- val (result, decorations) = server.resources.output_pretty_with_decorations(body, margin.value)
- output(result, Some(decorations))
- }
+ val (result, decorations) = server.resources.output_pretty_panel(body, margin.value)
+ output(result, decorations)
})
def locate(): Unit = print_state.locate_query()
--- a/src/Tools/VSCode/src/vscode_resources.scala Wed Jun 12 20:54:11 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala Wed Jun 12 21:22:01 2024 +0200
@@ -343,35 +343,47 @@
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)
- def output_pretty_with_decorations(
- body: XML.Body,
- margin: Double,
- ): (String, List[(String, List[LSP.Decoration_Options])]) = {
- val separate = Pretty.separate(body)
- val formatted = Pretty.formatted(separate, margin = margin)
-
- 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(unicode_symbols, content))
- }
- }
+ def output_pretty_panel(body: XML.Body, margin: Double): (String, Option[LSP.Decoration_List]) = {
+ val formatted = Pretty.formatted(Pretty.separate(body), margin = margin, metric = Symbol.Metric)
- val tree = Markup_Tree.from_XML(convert_symbols(formatted))
- val output = output_pretty(separate, margin = margin)
+ 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 html = node_context.make_html(elements, formatted)
+ (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(unicode_symbols, content))
+ }
+ }
- val document = Line.Document(output)
- 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
+ val tree = Markup_Tree.from_XML(convert_symbols(formatted))
+ val output = output_text(XML.content(formatted))
- (output, decorations)
+ val document = Line.Document(output)
+ 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, Some(decorations))
+ }
}