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) })