# HG changeset patch
# User wenzelm
# Date 1735223061 -3600
# Node ID 4210fd10e7769d3b423d0f1973d763183c6e0eb1
# Parent 7593c0976dc6865968e6f2a44e73b2612249ebf5
clarified signature;
diff -r 7593c0976dc6 -r 4210fd10e776 src/Pure/GUI/gui.scala
--- 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.output(text) + ""
+ else Style_HTML.enclose_text(text)
/* icon */
diff -r 7593c0976dc6 -r 4210fd10e776 src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala Thu Dec 26 15:18:19 2024 +0100
+++ b/src/Pure/Tools/doc.scala Thu Dec 26 15:24:21 2024 +0100
@@ -18,7 +18,8 @@
def view(): Unit = Doc.view(path)
override def toString: String = // GUI label
if (title.nonEmpty) {
- "" + HTML.output(name) + ": " + HTML.output(title) + ""
+ val style = GUI.Style_HTML
+ style.enclose(style.make_bold(name) + style.make_text(": " + title))
}
else name
}
diff -r 7593c0976dc6 -r 4210fd10e776 src/Tools/Graphview/tree_panel.scala
--- a/src/Tools/Graphview/tree_panel.scala Thu Dec 26 15:18:19 2024 +0100
+++ b/src/Tools/Graphview/tree_panel.scala Thu Dec 26 15:24:21 2024 +0100
@@ -128,7 +128,7 @@
})
private val selection_apply = new Button {
- action = Action("Apply") { selection_action () }
+ action = Action(GUI.Style_HTML.enclose_bold("Apply")) { selection_action () }
tooltip = "Apply tree selection to graph"
}
diff -r 7593c0976dc6 -r 4210fd10e776 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala Thu Dec 26 15:18:19 2024 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Thu Dec 26 15:24:21 2024 +0100
@@ -30,8 +30,10 @@
private val html =
item.description match {
case a :: bs =>
- "" + HTML.output(Symbol.print_newlines(a)) + "" +
- HTML.output(bs.map(b => " " + Symbol.print_newlines(b)).mkString) + ""
+ val style = GUI.Style_HTML
+ style.enclose(
+ style.make_bold(Symbol.print_newlines(a)) +
+ style.make_text(bs.map(b => " " + Symbol.print_newlines(b)).mkString))
case Nil => ""
}
override def toString: String = html
diff -r 7593c0976dc6 -r 4210fd10e776 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala Thu Dec 26 15:18:19 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Thu Dec 26 15:24:21 2024 +0100
@@ -216,7 +216,7 @@
}
private val eval_button =
- new GUI.Button("Eval") {
+ new GUI.Button(GUI.Style_HTML.enclose_bold("Eval")) {
tooltip = "Evaluate ML expression within optional context"
override def clicked(): Unit = eval_expression()
}
diff -r 7593c0976dc6 -r 4210fd10e776 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala Thu Dec 26 15:18:19 2024 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala Thu Dec 26 15:24:21 2024 +0100
@@ -272,7 +272,7 @@
}
private val build_button =
- new GUI.Button("Build") {
+ new GUI.Button(GUI.Style_HTML.enclose_bold("Build")) {
tooltip = "Build document"
override def clicked(): Unit = pending_process()
}
diff -r 7593c0976dc6 -r 4210fd10e776 src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala Thu Dec 26 15:18:19 2024 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala Thu Dec 26 15:24:21 2024 +0100
@@ -108,7 +108,7 @@
override def clicked(): Unit = apply_query()
}
- private val apply_button = new GUI.Button("Apply") {
+ private val apply_button = new GUI.Button(GUI.Style_HTML.enclose_bold("Apply")) {
tooltip = "Find theorems meeting specified criteria"
override def clicked(): Unit = apply_query()
}
@@ -155,7 +155,7 @@
/* GUI page */
- private val apply_button = new GUI.Button("Apply") {
+ private val apply_button = new GUI.Button(GUI.Style_HTML.enclose_bold("Apply")) {
tooltip = "Find constants by name / type patterns"
override def clicked(): Unit = apply_query()
}
@@ -226,7 +226,7 @@
/* GUI page */
- private val apply_button = new GUI.Button("Apply") {
+ private val apply_button = new GUI.Button(GUI.Style_HTML.enclose_bold("Apply")) {
tooltip = "Apply to current context"
override def clicked(): Unit = apply_query()
diff -r 7593c0976dc6 -r 4210fd10e776 src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu Dec 26 15:18:19 2024 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu Dec 26 15:24:21 2024 +0100
@@ -96,7 +96,7 @@
tooltip = "Try standard proof methods like \"auto\" and \"blast\" as alternatives to \"metis\""
}
- private val apply_query = new GUI.Button("Apply") {
+ private val apply_query = new GUI.Button(GUI.Style_HTML.enclose_bold("Apply")) {
tooltip = "Search for first-order proof using automatic theorem provers"
override def clicked(): Unit = hammer()
}
diff -r 7593c0976dc6 -r 4210fd10e776 src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala Thu Dec 26 15:18:19 2024 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala Thu Dec 26 15:24:21 2024 +0100
@@ -76,7 +76,7 @@
private val auto_hovering_button = new JEdit_Options.auto_hovering.GUI
- private val update_button = new GUI.Button("Update") {
+ private val update_button = new GUI.Button(GUI.Style_HTML.enclose_bold("Update")) {
tooltip = "Update display according to the command at cursor position"
override def clicked(): Unit = update_request()
}
diff -r 7593c0976dc6 -r 4210fd10e776 src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala Thu Dec 26 15:18:19 2024 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Thu Dec 26 15:24:21 2024 +0100
@@ -32,7 +32,7 @@
def update_font(): Unit = { font = GUI.font(size = font_size) }
update_font()
- text = "" + HTML.output(Symbol.decode(txt)) + ""
+ text = GUI.Style_HTML.enclose_text(Symbol.decode(txt))
action =
Action(text) {
val text_area = view.getTextArea