# HG changeset patch
# User wenzelm
# Date 1735217050 -3600
# Node ID 775514416939ff69871641f5b06ccb555dbbcffc
# Parent f13d04506126851a75f081b16c9bf6e69363b895
clarified signature;
diff -r f13d04506126 -r 775514416939 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala Thu Dec 26 13:22:28 2024 +0100
+++ b/src/Pure/GUI/gui.scala Thu Dec 26 13:44:10 2024 +0100
@@ -67,37 +67,58 @@
}
- /* named items */
+ /* style */
- enum Style { case plain, html, symbol_encoded, symbol_decoded }
+ class Style {
+ def enclose(body: String): String = body
+ def make_text(str: String): String = str
+ def make_bold(str: String): String = str
+ }
- def make_text(str: String, style: Style = Style.plain): String =
- if (style == Style.html) HTML.output(str) else str
+ class Style_HTML extends Style {
+ override def enclose(body: String): String = "" + body + ""
+ override def make_text(str: String): String = HTML.output(str)
+ override def make_bold(str: String): String = "" + make_text(str) + ""
+ }
- def make_bold(str: String, style: Style = Style.plain): String =
- style match {
- case Style.plain => str
- case Style.html => "" + HTML.output(str) + ""
- case _ =>
- 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
- }
+ abstract class Style_Symbol extends Style {
+ def bold: String
+ override def make_bold(str: String): String =
+ Symbol.iterator(str)
+ .flatMap(s => if (Symbol.is_controllable(s)) List(bold, s) else List(s))
+ .mkString
+ }
+
+ object Style_Plain extends Style { override def toString: String = "plain" }
+
+ object Style_HTML extends Style_HTML { override def toString: String = "html" }
+
+ object Style_Symbol_Encoded extends Style_Symbol {
+ override def toString: String = "symbol_encoded"
+ override def bold: String = Symbol.bold
+ }
+
+ object Style_Symbol_Decoded extends Style_Symbol {
+ override def toString: String = "symbol_decoded"
+ override def bold: String = Symbol.bold_decoded
+ }
+
+
+ /* named items */
sealed case class Name(
name: String,
kind: String = "",
prefix: String = "",
- style: Style = Style.plain
+ style: Style = Style_Plain
) {
override def toString: String = {
val a = kind.nonEmpty
val b = name.nonEmpty
- make_text(prefix, style = style) +
+ style.make_text(prefix) +
if_proper(a || b,
- if_proper(prefix, ": ") + if_proper(kind, make_bold(kind, style = style)) +
- if_proper(a && b, " ") + if_proper(b, make_text(quote(name), style = style)))
+ if_proper(prefix, ": ") + if_proper(kind, style.make_bold(kind)) +
+ if_proper(a && b, " ") + if_proper(b, style.make_text(quote(name))))
}
}
diff -r f13d04506126 -r 775514416939 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala Thu Dec 26 13:22:28 2024 +0100
+++ b/src/Pure/PIDE/rendering.scala Thu Dec 26 13:44:10 2024 +0100
@@ -162,7 +162,7 @@
def gui_name(name: String, kind: String = "", prefix: String = ""): String =
GUI.Name(name, kind = Word.informal(kind), prefix = prefix,
- style = GUI.Style.symbol_decoded).toString
+ style = GUI.Style_Symbol_Decoded).toString
def get_tooltip_description(name: String): Option[String] = tooltip_description.get(name)