--- a/src/Tools/VSCode/src/dynamic_output.scala Fri Feb 25 16:12:42 2022 +0100
+++ b/src/Tools/VSCode/src/dynamic_output.scala Fri Feb 25 16:54:50 2022 +0100
@@ -35,25 +35,19 @@
else this
}
if (st1.output != output) {
- val elements = Presentation.Elements(
- html = Presentation.elements2.html,
- language = Presentation.elements2.language,
- entity = Markup.Elements.full)
-
- def entity_link(props: Properties.T, body: XML.Body): Option[XML.Tree] =
- for {
- thy_file <- Position.Def_File.unapply(props)
- def_line <- Position.Def_Line.unapply(props)
- source <- resources.source_file(thy_file)
- uri = Path.explode(source).absolute_file.toURI
- } yield HTML.link(uri.toString + "#" + def_line, body)
-
- val htmlBody = Presentation.make_html(
- Presentation.Entity_Context.empty, // FIXME
- elements,
- Pretty.separate(st1.output))
-
- channel.write(LSP.Dynamic_Output(HTML.source(htmlBody).toString))
+ val context =
+ new Presentation.Entity_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 = Path.explode(source).absolute_file.toURI
+ } yield HTML.link(uri.toString + "#" + def_line, body)
+ }
+ val elements = Presentation.elements2.copy(entity = Markup.Elements.full)
+ val html = Presentation.make_html(context, elements, Pretty.separate(st1.output))
+ channel.write(LSP.Dynamic_Output(HTML.source(html).toString))
}
st1
}