# HG changeset patch
# User wenzelm
# Date 1735317602 -3600
# Node ID af2fb968b6bd1fcaebcd04675d1d727e2683a454
# Parent  b18330f7bde076cb020fbfd2e303b7df3c51ac64
tuned generated output: more standard operations;

diff -r b18330f7bde0 -r af2fb968b6bd 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