--- a/src/Pure/GUI/gui.scala Thu Dec 26 15:18:19 2024 +0100
+++ b/src/Pure/GUI/gui.scala Thu Dec 26 15:24:21 2024 +0100
@@ -73,6 +73,8 @@
def enclose(body: String): String = body
def make_text(str: String): String = str
def make_bold(str: String): String = str
+ def enclose_text(str: String): String = enclose(make_text(str))
+ def enclose_bold(str: String): String = enclose(make_bold(str))
}
class Style_HTML extends Style {
@@ -319,7 +321,7 @@
def tooltip_lines(text: String): String =
if (text == null || text == "") null
- else "<html>" + HTML.output(text) + "</html>"
+ else Style_HTML.enclose_text(text)
/* icon */