# HG changeset patch
# User wenzelm
# Date 1735211036 -3600
# Node ID e4152e64698f2879c5b7f234a74e5a985e07a3ce
# Parent  904b2144e9c594dc9f1b2c86b919b694a3a0b83e
clarified signature;

diff -r 904b2144e9c5 -r e4152e64698f src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Tue Dec 24 16:57:28 2024 +0100
+++ b/src/Pure/GUI/gui.scala	Thu Dec 26 12:03:56 2024 +0100
@@ -69,14 +69,14 @@
 
   /* named items */
 
-  enum Style { case plain, html, symbol, symbol_decoded }
+  enum Style { case plain, html, symbol_encoded, symbol_decoded }
 
   def make_bold(str: String, style: Style = Style.plain): String =
     style match {
       case Style.plain => str
       case Style.html => "<b>" + HTML.output(str) + "</b>"
       case _ =>
-        val b = if (style == Style.symbol) Symbol.bold else Symbol.bold_decoded
+        val b = if (style == Style.symbol_encoded) Symbol.bold else Symbol.bold_decoded
         Symbol.iterator(str)
           .flatMap(s => if (Symbol.is_controllable(s)) List(b, s) else List(s))
           .mkString