tuned generated output: more standard operations;
authorwenzelm
Fri, 27 Dec 2024 17:40:02 +0100
changeset 81672 af2fb968b6bd
parent 81671 b18330f7bde0
child 81673 68a9ada23bf8
tuned generated output: more standard operations;
src/Tools/jEdit/jedit_main/isabelle_sidekick.scala
--- a/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala	Fri Dec 27 17:35:24 2024 +0100
+++ b/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala	Fri Dec 27 17:40:02 2024 +0100
@@ -32,6 +32,7 @@
   }
 
   class Keyword_Asset(keyword: String, text: String, range: Text.Range) extends IAsset {
+    private val style = GUI.Style_HTML
     private val css = GUI.imitate_font_css(GUI.label_font())
 
     protected var _name: String = text
@@ -43,12 +44,12 @@
       val s =
         _name.indexOf(keyword) match {
           case i if i >= 0 && n > 0 =>
-            HTML.output(_name.substring(0, i)) +
-            "<b>" + HTML.output(keyword) + "</b>" +
-            HTML.output(_name.substring(i + n))
-          case _ => HTML.output(_name)
+            style.make_text(_name.substring(0, i)) +
+            style.make_bold(keyword) +
+            style.make_text(_name.substring(i + n))
+          case _ => style.make_text(_name)
         }
-      GUI.Style_HTML.enclose_style(css, s)
+      style.enclose_style(css, s)
     }
     override def getLongString: String = _name
     override def getName: String = _name