tuned GUI output: more uniform;
authorwenzelm
Fri, 27 Dec 2024 17:35:24 +0100
changeset 81671 b18330f7bde0
parent 81670 3e51429404cd
child 81672 af2fb968b6bd
tuned GUI output: more uniform;
src/Tools/jEdit/jedit_main/isabelle_sidekick.scala
--- a/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala	Fri Dec 27 17:30:59 2024 +0100
+++ b/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala	Fri Dec 27 17:35:24 2024 +0100
@@ -272,6 +272,7 @@
     val data = Isabelle_Sidekick.root_data(buffer)
 
     try {
+      val style = GUI.Style_HTML
       var offset = 0
       for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) {
         val kind = chunk.kind
@@ -279,9 +280,7 @@
         val source = chunk.source
         if (kind != "") {
           val label = kind + if_proper(name, " " + name)
-          val label_html =
-            "<html><b>" + HTML.output(kind) + "</b>" +
-            if_proper(name, " " + HTML.output(name)) + "</html>"
+          val label_html = style.enclose(GUI.Name(name, kind = kind, style = style).toString)
           val range = Text.Range(offset, offset + source.length)
           val asset = new Asset(label, label_html, range, source)
           data.root.add(Tree_View.Node(asset))