# HG changeset patch
# User wenzelm
# Date 1645804490 -3600
# Node ID 3b5aa38282bd72e417699c3e416acdf2e5e8be23
# Parent  e7b7764d0977e423c8f9b6a480dcac76d2175330
proper Presentation.Entity_Context for hyperlinks (amending da1108a6d249);

diff -r e7b7764d0977 -r 3b5aa38282bd src/Tools/VSCode/src/dynamic_output.scala
--- 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
     }
diff -r e7b7764d0977 -r 3b5aa38282bd src/Tools/VSCode/src/state_panel.scala
--- a/src/Tools/VSCode/src/state_panel.scala	Fri Feb 25 16:12:42 2022 +0100
+++ b/src/Tools/VSCode/src/state_panel.scala	Fri Feb 25 16:54:50 2022 +0100
@@ -63,25 +63,19 @@
     new Query_Operation(server.editor, (), "print_state", _ => (),
       (_, _, body) =>
         if (output_active.value && body.nonEmpty){
-          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 <- server.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(body))
-
-          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 <- server.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(body))
+          output(HTML.source(html).toString)
         })
 
   def locate(): Unit = print_state.locate_query()