src/Tools/VSCode/src/state_panel.scala
changeset 75928 fa8d9e5ef913
parent 75927 040a59abe196
child 75941 4bbbbaa656f1
--- a/src/Tools/VSCode/src/state_panel.scala	Sat Aug 20 17:01:34 2022 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala	Sat Aug 20 17:25:55 2022 +0200
@@ -70,7 +70,7 @@
                 } yield HTML.link(uri.toString + "#" + def_line, body)
             }
           val elements = Presentation.elements2.copy(entity = Markup.Elements.full)
-          val html = Presentation.make_html(node_context, elements, Pretty.separate(body))
+          val html = node_context.make_html(elements, Pretty.separate(body))
           output(HTML.source(html).toString)
         })