# HG changeset patch # User wenzelm # Date 1735325875 -3600 # Node ID ece4941f0f1786e9c0c268ca3f62e46ff797fd82 # Parent 0ca0a47235e53ec93bce681e2a149726b829db61# Parent 70d2f72098df74a3781d46fd7ba60d652ba4c4b9 merged diff -r 0ca0a47235e5 -r ece4941f0f17 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Mon Dec 23 21:58:26 2024 +0100 +++ b/Admin/components/components.sha1 Fri Dec 27 19:57:55 2024 +0100 @@ -153,6 +153,7 @@ 9467ad54a9ac10a6e7e8db5458d8d2a5516eba96 isabelle_fonts-20210321.tar.gz 1f7a0b9829ecac6552b21e995ad0f0ac168634f3 isabelle_fonts-20210322.tar.gz 667000ce6dd6ea3c2d11601a41c206060468807d isabelle_fonts-20211004.tar.gz +1d16542fa847c65ae137adb723da3afbbe252abf isabelle_fonts-20241227.tar.gz 916adccd2f40c55116b68b92ce1eccb24d4dd9a2 isabelle_setup-20210630.tar.gz c611e363287fcc9bdd93c33bef85fa4e66cd3f37 isabelle_setup-20210701.tar.gz a0e7527448ef0f7ce164a38a50dc26e98de3cad6 isabelle_setup-20210709.tar.gz diff -r 0ca0a47235e5 -r ece4941f0f17 Admin/components/main --- a/Admin/components/main Mon Dec 23 21:58:26 2024 +0100 +++ b/Admin/components/main Fri Dec 27 19:57:55 2024 +0100 @@ -10,7 +10,7 @@ flatlaf-2.6 foiltex-2.1.4b idea-icons-20210508 -isabelle_fonts-20211004 +isabelle_fonts-20241227 isabelle_setup-20240327 javamail-20240109 jdk-21.0.5 diff -r 0ca0a47235e5 -r ece4941f0f17 src/HOL/HOLCF/Algebraic.thy --- a/src/HOL/HOLCF/Algebraic.thy Mon Dec 23 21:58:26 2024 +0100 +++ b/src/HOL/HOLCF/Algebraic.thy Fri Dec 27 19:57:55 2024 +0100 @@ -47,11 +47,11 @@ by (rule Rep_fin_defl.belowD) lemma fin_defl_eqI: - "(\x. Rep_fin_defl a\x = x \ Rep_fin_defl b\x = x) \ a = b" -apply (rule below_antisym) -apply (rule fin_defl_belowI, simp) -apply (rule fin_defl_belowI, simp) -done + "a = b" if "(\x. Rep_fin_defl a\x = x \ Rep_fin_defl b\x = x)" +proof (rule below_antisym) + show "a \ b" by (rule fin_defl_belowI) (simp add: that) + show "b \ a" by (rule fin_defl_belowI) (simp add: that) +qed lemma Rep_fin_defl_mono: "a \ b \ Rep_fin_defl a \ Rep_fin_defl b" unfolding below_fin_defl_def . @@ -63,8 +63,8 @@ by (simp add: Abs_fin_defl_inverse) lemma (in finite_deflation) compact_belowI: - assumes "\x. compact x \ d\x = x \ f\x = x" shows "d \ f" -by (rule belowI, rule assms, erule subst, rule compact) + "d \ f" if "\x. compact x \ d\x = x \ f\x = x" + by (rule belowI, rule that, erule subst, rule compact) lemma compact_Rep_fin_defl [simp]: "compact (Rep_fin_defl a)" using finite_deflation_Rep_fin_defl @@ -79,10 +79,10 @@ instantiation defl :: (bifinite) below begin -definition - "x \ y \ Rep_defl x \ Rep_defl y" +definition "x \ y \ Rep_defl x \ Rep_defl y" instance .. + end instance defl :: (bifinite) po @@ -93,9 +93,8 @@ using type_definition_defl below_defl_def by (rule below.typedef_ideal_cpo) -definition - defl_principal :: "'a::bifinite fin_defl \ 'a defl" where - "defl_principal t = Abs_defl {u. u \ t}" +definition defl_principal :: "'a::bifinite fin_defl \ 'a defl" + where "defl_principal t = Abs_defl {u. u \ t}" lemma fin_defl_countable: "\f::'a::bifinite fin_defl \ nat. inj f" proof - @@ -134,11 +133,13 @@ text \Algebraic deflations are pointed\ lemma defl_minimal: "defl_principal (Abs_fin_defl \) \ x" -apply (induct x rule: defl.principal_induct, simp) -apply (rule defl.principal_mono) -apply (simp add: below_fin_defl_def) -apply (simp add: Abs_fin_defl_inverse finite_deflation_bottom) -done +proof (induct x rule: defl.principal_induct) + fix a :: "'a fin_defl" + have "Abs_fin_defl \ \ a" + by (simp add: below_fin_defl_def Abs_fin_defl_inverse finite_deflation_bottom) + then show "defl_principal (Abs_fin_defl \) \ defl_principal a" + by (rule defl.principal_mono) +qed simp instance defl :: (bifinite) pcpo by intro_classes (fast intro: defl_minimal) @@ -149,17 +150,12 @@ subsection \Applying algebraic deflations\ -definition - cast :: "'a::bifinite defl \ 'a \ 'a" -where - "cast = defl.extension Rep_fin_defl" +definition cast :: "'a::bifinite defl \ 'a \ 'a" + where "cast = defl.extension Rep_fin_defl" -lemma cast_defl_principal: - "cast\(defl_principal a) = Rep_fin_defl a" -unfolding cast_def -apply (rule defl.extension_principal) -apply (simp only: below_fin_defl_def) -done +lemma cast_defl_principal: "cast\(defl_principal a) = Rep_fin_defl a" + unfolding cast_def + by (rule defl.extension_principal) (simp only: below_fin_defl_def) lemma deflation_cast: "deflation (cast\d)" apply (induct d rule: defl.principal_induct) @@ -169,22 +165,20 @@ apply (rule finite_deflation_Rep_fin_defl) done -lemma finite_deflation_cast: - "compact d \ finite_deflation (cast\d)" -apply (drule defl.compact_imp_principal, clarify) -apply (simp add: cast_defl_principal) -apply (rule finite_deflation_Rep_fin_defl) -done +lemma finite_deflation_cast: "compact d \ finite_deflation (cast\d)" + apply (drule defl.compact_imp_principal) + apply clarify + apply (simp add: cast_defl_principal) + apply (rule finite_deflation_Rep_fin_defl) + done interpretation cast: deflation "cast\d" by (rule deflation_cast) declare cast.idem [simp] -lemma compact_cast [simp]: "compact d \ compact (cast\d)" -apply (rule finite_deflation_imp_compact) -apply (erule finite_deflation_cast) -done +lemma compact_cast [simp]: "compact (cast\d)" if "compact d" + by (rule finite_deflation_imp_compact) (use that in \rule finite_deflation_cast\) lemma cast_below_cast: "cast\A \ cast\B \ A \ B" apply (induct A rule: defl.principal_induct, simp) @@ -236,10 +230,13 @@ assumes f: "\a. finite_deflation a \ finite_deflation (f\a)" shows "cast\(defl_fun1 e p f\A) = e oo f\(cast\A) oo p" proof - - have 1: "\a. finite_deflation (e oo f\(Rep_fin_defl a) oo p)" - apply (rule ep_pair.finite_deflation_e_d_p [OF ep]) - apply (rule f, rule finite_deflation_Rep_fin_defl) - done + have 1: "finite_deflation (e oo f\(Rep_fin_defl a) oo p)" for a + proof - + have "finite_deflation (f\(Rep_fin_defl a))" + using finite_deflation_Rep_fin_defl by (rule f) + with ep show ?thesis + by (rule ep_pair.finite_deflation_e_d_p) + qed show ?thesis by (induct A rule: defl.principal_induct, simp) (simp only: defl_fun1_def @@ -259,11 +256,13 @@ finite_deflation (f\a\b)" shows "cast\(defl_fun2 e p f\A\B) = e oo f\(cast\A)\(cast\B) oo p" proof - - have 1: "\a b. finite_deflation - (e oo f\(Rep_fin_defl a)\(Rep_fin_defl b) oo p)" - apply (rule ep_pair.finite_deflation_e_d_p [OF ep]) - apply (rule f, (rule finite_deflation_Rep_fin_defl)+) - done + have 1: "finite_deflation (e oo f\(Rep_fin_defl a)\(Rep_fin_defl b) oo p)" for a b + proof - + have "finite_deflation (f\(Rep_fin_defl a)\(Rep_fin_defl b))" + using finite_deflation_Rep_fin_defl finite_deflation_Rep_fin_defl by (rule f) + with ep show ?thesis + by (rule ep_pair.finite_deflation_e_d_p) + qed show ?thesis apply (induct A rule: defl.principal_induct, simp) apply (induct B rule: defl.principal_induct, simp) diff -r 0ca0a47235e5 -r ece4941f0f17 src/Pure/Admin/component_fonts.scala --- a/src/Pure/Admin/component_fonts.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Pure/Admin/component_fonts.scala Fri Dec 27 19:57:55 2024 +0100 @@ -24,6 +24,8 @@ 0x201c, // double quote 0x201d, // double quote 0x201e, // double quote + 0x2022, // regular bullet + 0x2023, // triangular bullet 0x2039, // single guillemet 0x203a, // single guillemet 0x204b, // FOOTNOTE @@ -58,7 +60,6 @@ 0x2016, // big parallel 0x2020, // dagger 0x2021, // double dagger - 0x2022, // bullet 0x2026, // ellipsis 0x2030, // perthousand 0x2032, // minute diff -r 0ca0a47235e5 -r ece4941f0f17 src/Pure/Admin/component_llncs.scala --- a/src/Pure/Admin/component_llncs.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Pure/Admin/component_llncs.scala Fri Dec 27 19:57:55 2024 +0100 @@ -59,7 +59,7 @@ /* README */ - File.change(component_dir.path + README_md)(_.replace(" ", "\u00a0")) + File.change(component_dir.path + README_md)(_.replace(" ", HTML.space)) File.write(component_dir.README, """This is the Springer LaTeX LNCS style for authors from diff -r 0ca0a47235e5 -r ece4941f0f17 src/Pure/Concurrent/delay.scala --- a/src/Pure/Concurrent/delay.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Pure/Concurrent/delay.scala Fri Dec 27 19:57:55 2024 +0100 @@ -20,7 +20,7 @@ final class Delay private(first: Boolean, delay: => Time, log: Logger, event: => Unit) { private var running: Option[Event_Timer.Request] = None - private def run: Unit = { + private def run(): Unit = { val do_run = synchronized { if (running.isDefined) { running = None; true } else false } @@ -37,8 +37,9 @@ case Some(request) => if (first) false else { request.cancel(); true } case None => true } - if (new_run) - running = Some(Event_Timer.request(Time.now() + delay)(run)) + if (new_run) { + running = Some(Event_Timer.request(Time.now() + delay)(run())) + } } def revoke(msg: String = ""): Unit = synchronized { @@ -55,7 +56,7 @@ case Some(request) => val alt_time = Time.now() + alt_delay if (request.time < alt_time && request.cancel()) { - running = Some(Event_Timer.request(alt_time)(run)) + running = Some(Event_Timer.request(alt_time)(run())) } case None => } diff -r 0ca0a47235e5 -r ece4941f0f17 src/Pure/Concurrent/event_timer.scala --- a/src/Pure/Concurrent/event_timer.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Pure/Concurrent/event_timer.scala Fri Dec 27 19:57:55 2024 +0100 @@ -25,7 +25,7 @@ } def request(time: Time, repeat: Option[Time] = None)(event: => Unit): Request = { - val task = new TimerTask { def run: Unit = event } + val task = new TimerTask { def run(): Unit = event } repeat match { case None => event_timer.schedule(task, new JDate(time.ms)) case Some(rep) => event_timer.schedule(task, new JDate(time.ms), rep.ms) diff -r 0ca0a47235e5 -r ece4941f0f17 src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Pure/GUI/gui.scala Fri Dec 27 19:57:55 2024 +0100 @@ -67,6 +67,89 @@ } + /* style */ + + class Style { + 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)) + def spaces(n: Int): String = Symbol.spaces(n) + } + + class Style_HTML extends Style { + override def enclose(body: String): String = enclose_style("", body) + override def make_text(str: String): String = HTML.output(str) + override def make_bold(str: String): String = "" + make_text(str) + "" + override def spaces(n: Int): String = HTML.spaces(n) + + def enclose_style(style: String, body: String): String = + if (style.isEmpty) { + Library.string_builder(body.length + 13) { s => + s ++= "" + s ++= body + s ++= "" + } + } + else { + Library.string_builder(style.length + body.length + 35) { s => + s ++= "" + s ++= body + s ++= "" + } + } + + def regular_bullet: String = "\u2022" + def triangular_bullet: String = "\u2023" + } + + 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 + ) { + def set_style(new_style: Style): Name = copy(style = new_style) + + override def toString: String = { + val a = kind.nonEmpty + val b = name.nonEmpty + style.make_text(prefix) + + if_proper(a || b, + if_proper(prefix, ": ") + if_proper(kind, style.make_bold(kind)) + + if_proper(a && b, " ") + if_proper(b, style.make_text(quote(name)))) + } + } + + /* simple dialogs */ def scrollable_text( @@ -263,7 +346,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 0ca0a47235e5 -r ece4941f0f17 src/Pure/General/completion.scala --- a/src/Pure/General/completion.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Pure/General/completion.scala Fri Dec 27 19:57:55 2024 +0100 @@ -198,8 +198,7 @@ if (kind == "") (name, quote(decode(name))) else (Long_Name.qualify(kind, name), - Word.implode(Word.explode('_', kind)) + - (if (xname == name) "" else " " + quote(decode(name)))) + Word.informal(kind) + (if (xname == name) "" else " " + quote(decode(name)))) } yield { val description = List(xname1, "(" + descr_name + ")") val replacement = diff -r 0ca0a47235e5 -r ece4941f0f17 src/Pure/General/html.scala --- a/src/Pure/General/html.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Pure/General/html.scala Fri Dec 27 19:57:55 2024 +0100 @@ -7,11 +7,28 @@ package isabelle +import java.awt.Color +import java.util.Locale + import org.jsoup.nodes.{Entities => Jsoup_Entities, Document => Jsoup_Document} import org.jsoup.Jsoup object HTML { + /* spaces (non-breaking) */ + + val space = "\u00a0" + + private val static_spaces = space * 100 + + def spaces(n: Int): String = { + require(n >= 0, "negative spaces") + if (n == 0) "" + else if (n < static_spaces.length) static_spaces.substring(0, n) + else space * n + } + + /* attributes */ class Attribute(val name: String, value: String) { @@ -97,6 +114,21 @@ def script_file(href: String): XML.Elem = XML.Elem(Markup("script", List("src" -> href)), Nil) def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file)) + def color(c: Color): String = { + val r = Integer.valueOf(c.getRed) + val g = Integer.valueOf(c.getGreen) + val b = Integer.valueOf(c.getBlue) + c.getAlpha match { + case 255 => String.format(Locale.ROOT, "rgb(%d,%d,%d)", r, g, b) + case a => + String.format(Locale.ROOT, "rgba(%d,%d,%d,%.2f)", r, g, b, + java.lang.Double.valueOf(a.toDouble / 255)) + } + } + + def color_property(c: Color): String = "color: " + color(c) + def background_property(c: Color): String = "background: " + color(c) + /* href */ diff -r 0ca0a47235e5 -r ece4941f0f17 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Pure/General/symbol.scala Fri Dec 27 19:57:55 2024 +0100 @@ -25,18 +25,17 @@ val space_char = ' ' val space = " " - private val static_spaces_length = 4000 - private val static_spaces = space * static_spaces_length + private val static_spaces = space * 4000 def is_static_spaces(s: String): Boolean = { val n = s.length - n == 0 || n <= static_spaces_length && s(0) == space_char && s.forall(_ == space_char) + n == 0 || n <= static_spaces.length && s(0) == space_char && s.forall(_ == space_char) } def spaces(n: Int): String = { require(n >= 0, "negative spaces") if (n == 0) "" - else if (n < static_spaces_length) static_spaces.substring(0, n) + else if (n < static_spaces.length) static_spaces.substring(0, n) else space * n } diff -r 0ca0a47235e5 -r ece4941f0f17 src/Pure/General/word.scala --- a/src/Pure/General/word.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Pure/General/word.scala Fri Dec 27 19:57:55 2024 +0100 @@ -76,6 +76,8 @@ def explode(text: String): List[String] = explode(Character.isWhitespace _, text) + def informal(text: String): String = implode(explode('_', text)) + /* brackets */ diff -r 0ca0a47235e5 -r ece4941f0f17 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Pure/PIDE/markup.scala Fri Dec 27 19:57:55 2024 +0100 @@ -238,7 +238,7 @@ def is_antiquotation: Boolean = name == Language.ANTIQUOTATION def is_path: Boolean = name == Language.PATH - def description: String = Word.implode(Word.explode('_', name)) + def description: String = Word.informal(name) } diff -r 0ca0a47235e5 -r ece4941f0f17 src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Pure/PIDE/rendering.scala Fri Dec 27 19:57:55 2024 +0100 @@ -160,6 +160,10 @@ /* tooltips */ + 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 + def get_tooltip_description(name: String): Option[String] = tooltip_description.get(name) private val tooltip_description = @@ -172,14 +176,6 @@ Markup.TFREE -> "free type variable", Markup.TVAR -> "schematic type variable") - def tooltip_text(markup: String, kind: String, name: String): String = { - val a = kind.nonEmpty - val b = name.nonEmpty - val k = Word.implode(Word.explode('_', kind)) - if (!a && !b) markup - else markup + ": " + k + if_proper(a && b, " ") + if_proper(b, quote(name)) - } - /* entity focus */ @@ -678,30 +674,25 @@ case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _))) if kind != "" && kind != Markup.ML_DEF => - val kind1 = Word.implode(Word.explode('_', kind)) - val txt1 = - if (name == "") kind1 - else if (kind1 == "") quote(name) - else kind1 + " " + quote(name) - val info1 = info.add_info_text(r0, txt1, ord = 2) + val txt = Rendering.gui_name(name, kind = kind) + val info1 = info.add_info_text(r0, txt, ord = 2) Some(if (kind == Markup.COMMAND) info1.add_info(r0, XML.elem(Markup.TIMING)) else info1) case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) => val file = perhaps_append_file(snapshot.node_name, name) val info1 = if (name == file) info - else info.add_info_text(r0, "path " + quote(name)) - Some(info1.add_info_text(r0, "file " + quote(file))) + else info.add_info_text(r0, Rendering.gui_name(name, kind = "path")) + Some(info1.add_info_text(r0, Rendering.gui_name(file, kind = "file"))) case (info, Text.Info(r0, XML.Elem(Markup.Doc(name), _))) => - val text = "doc " + quote(name) - Some(info.add_info_text(r0, text)) + Some(info.add_info_text(r0, Rendering.gui_name(name, kind = "doc"))) case (info, Text.Info(r0, XML.Elem(Markup.Url(name), _))) => - Some(info.add_info_text(r0, "URL " + quote(name))) + Some(info.add_info_text(r0, Rendering.gui_name(name, kind = "URL"))) case (info, Text.Info(r0, XML.Elem(Markup.Command_Span(span), _))) => - Some(info.add_info_text(r0, "command span " + quote(span.name))) + Some(info.add_info_text(r0, Rendering.gui_name(span.name, kind = Markup.COMMAND_SPAN))) case (info, Text.Info(r0, XML.Elem(Markup(name, _), body))) if name == Markup.SORTING || name == Markup.TYPING => @@ -724,11 +715,11 @@ Some(info.add_info_text(r0, "language: " + lang.description)) case (info, Text.Info(r0, XML.Elem(Markup.Notation(kind, name), _))) => - val description = Rendering.tooltip_text(Markup.NOTATION, kind, name) + val description = Rendering.gui_name(name, kind = kind, prefix = Markup.NOTATION) Some(info.add_info_text(r0, description, ord = 1)) case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind, name), _))) => - val description = Rendering.tooltip_text(Markup.EXPRESSION, kind, name) + val description = Rendering.gui_name(name, kind = kind, prefix = Markup.EXPRESSION) Some(info.add_info_text(r0, description, ord = 1)) case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) => diff -r 0ca0a47235e5 -r ece4941f0f17 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Pure/System/isabelle_system.scala Fri Dec 27 19:57:55 2024 +0100 @@ -390,7 +390,7 @@ /* JVM shutdown hook */ def create_shutdown_hook(body: => Unit): Thread = { - val shutdown_hook = Isabelle_Thread.create(new Runnable { def run: Unit = body }) + val shutdown_hook = Isabelle_Thread.create(new Runnable { def run(): Unit = body }) try { Runtime.getRuntime.addShutdownHook(shutdown_hook) } catch { case _: IllegalStateException => } diff -r 0ca0a47235e5 -r ece4941f0f17 src/Pure/Tools/doc.scala --- a/src/Pure/Tools/doc.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Pure/Tools/doc.scala Fri Dec 27 19:57:55 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 0ca0a47235e5 -r ece4941f0f17 src/Tools/Graphview/tree_panel.scala --- a/src/Tools/Graphview/tree_panel.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Tools/Graphview/tree_panel.scala Fri Dec 27 19:57:55 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 0ca0a47235e5 -r ece4941f0f17 src/Tools/jEdit/jedit_main/isabelle_sidekick.scala --- a/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala Fri Dec 27 19:57:55 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)) + - "" + HTML.output(keyword) + "" + - 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) } - "" + s + "" + style.enclose_style(css, s) } override def getLongString: String = _name override def getName: String = _name @@ -272,6 +273,7 @@ val data = Isabelle_Sidekick.root_data(buffer) try { + val style = GUI.Style_HTML var offset = 0 for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) { val kind = chunk.kind @@ -279,9 +281,7 @@ val source = chunk.source if (kind != "") { val label = kind + if_proper(name, " " + name) - val label_html = - "" + HTML.output(kind) + "" + - if_proper(name, " " + HTML.output(name)) + "" + val label_html = style.enclose(GUI.Name(name, kind = kind, style = style).toString) val range = Text.Range(offset, offset + source.length) val asset = new Asset(label, label_html, range, source) data.root.add(Tree_View.Node(asset)) diff -r 0ca0a47235e5 -r ece4941f0f17 src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Tools/jEdit/src/completion_popup.scala Fri Dec 27 19:57:55 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 0ca0a47235e5 -r ece4941f0f17 src/Tools/jEdit/src/debugger_dockable.scala --- a/src/Tools/jEdit/src/debugger_dockable.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Fri Dec 27 19:57:55 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 0ca0a47235e5 -r ece4941f0f17 src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Fri Dec 27 19:57:55 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 0ca0a47235e5 -r ece4941f0f17 src/Tools/jEdit/src/keymap_merge.scala --- a/src/Tools/jEdit/src/keymap_merge.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Tools/jEdit/src/keymap_merge.scala Fri Dec 27 19:57:55 2024 +0100 @@ -102,12 +102,14 @@ PIDE.options.color_value("error_color") private sealed case class Table_Entry(shortcut: Shortcut, head: Option[Int], tail: List[Int]) { - override def toString: String = - if (head.isEmpty) "" + HTML.output(shortcut.toString) + "" - else - "" + - HTML.output("--- " + shortcut.toString) + - "" + override def toString: String = { + val style = GUI.Style_HTML + if (head.isEmpty) style.enclose(style.make_text(shortcut.toString)) + else { + style.enclose_style(HTML.color_property(conflict_color), + style.make_text("--- " + shortcut.toString)) + } + } } private class Table_Model(entries: List[Table_Entry]) extends AbstractTableModel { diff -r 0ca0a47235e5 -r ece4941f0f17 src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Fri Dec 27 19:57:55 2024 +0100 @@ -42,6 +42,7 @@ ) { lazy val line_text: String = Library.trim_line(JEdit_Lib.get_text(buffer, line_range).getOrElse("")) + .replace('\t',' ') lazy val gui_text: String = Library.string_builder(line_range.length * 2) { s => // see also HyperSearchResults.highlightString @@ -50,20 +51,22 @@ s ++= ": " val line_start = line_range.start - val plain_text = line_text.replace('\t',' ').trim - val search_range = Text.Range(line_start, line_start + plain_text.length) - var last = 0 + val plain_start = line_text.length - line_text.stripLeading.length + val plain_stop = line_text.stripTrailing.length + + val search_range = Text.Range(line_start + plain_start, line_start + plain_stop) + var last = plain_start for (range <- JEdit_Lib.search_text(buffer, search_range, regex)) { val next = range.start - line_start - if (last < next) s ++= plain_text.substring(last, next) + if (last < next) s ++= line_text.substring(last, next) s ++= "" - s ++= plain_text.substring(next, next + range.length) + s ++= line_text.substring(next, next + range.length) s ++= "" last = range.stop - line_start } - if (last < plain_text.length) s ++= plain_text.substring(last) + if (last < plain_stop) s ++= line_text.substring(last) s ++= "" } override def toString: String = gui_text diff -r 0ca0a47235e5 -r ece4941f0f17 src/Tools/jEdit/src/query_dockable.scala --- a/src/Tools/jEdit/src/query_dockable.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Tools/jEdit/src/query_dockable.scala Fri Dec 27 19:57:55 2024 +0100 @@ -10,9 +10,9 @@ import isabelle._ import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent} -import javax.swing.{JComponent, JTextField} +import javax.swing.JComponent -import scala.swing.{Component, TextField, Label, ListView, TabbedPane, BorderPanel} +import scala.swing.{Component, TextField, Label, TabbedPane, BorderPanel} import scala.swing.event.{SelectionChanged, Key, KeyPressed} import org.gjt.sp.jedit.View @@ -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 0ca0a47235e5 -r ece4941f0f17 src/Tools/jEdit/src/sledgehammer_dockable.scala --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Fri Dec 27 19:57:55 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 0ca0a47235e5 -r ece4941f0f17 src/Tools/jEdit/src/state_dockable.scala --- a/src/Tools/jEdit/src/state_dockable.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Tools/jEdit/src/state_dockable.scala Fri Dec 27 19:57:55 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 0ca0a47235e5 -r ece4941f0f17 src/Tools/jEdit/src/symbols_dockable.scala --- a/src/Tools/jEdit/src/symbols_dockable.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Fri Dec 27 19:57:55 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 diff -r 0ca0a47235e5 -r ece4941f0f17 src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Tools/jEdit/src/theories_dockable.scala Fri Dec 27 19:57:55 2024 +0100 @@ -9,9 +9,9 @@ import isabelle._ -import scala.swing.{Button, TextArea, Label, ListView, ScrollPane, Component} +import scala.swing.{Button, Label, ScrollPane} -import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension} +import java.awt.BorderLayout import javax.swing.border.{BevelBorder, SoftBevelBorder} import org.gjt.sp.jedit.{View, jEdit} diff -r 0ca0a47235e5 -r ece4941f0f17 src/Tools/jEdit/src/timing_dockable.scala --- a/src/Tools/jEdit/src/timing_dockable.scala Mon Dec 23 21:58:26 2024 +0100 +++ b/src/Tools/jEdit/src/timing_dockable.scala Fri Dec 27 19:57:55 2024 +0100 @@ -28,68 +28,60 @@ entry2.timing compare entry1.timing } - object Renderer_Component extends Label { - opaque = false - xAlignment = Alignment.Leading - border = BorderFactory.createEmptyBorder(2, 2, 2, 2) - - var entry: Entry = null - override def paintComponent(gfx: Graphics2D): Unit = { - def paint_rectangle(color: Color): Unit = { - val size = peer.getSize() - val insets = border.getBorderInsets(peer) - val x = insets.left - val y = insets.top - val w = size.width - x - insets.right - val h = size.height - y - insets.bottom - gfx.setColor(color) - gfx.fillRect(x, y, w, h) - } - - entry match { - case theory_entry: Theory_Entry if theory_entry.current => - paint_rectangle(view.getTextArea.getPainter.getSelectionColor) - case _: Command_Entry => - paint_rectangle(view.getTextArea.getPainter.getMultipleSelectionColor) - case _ => - } - super.paintComponent(gfx) - } - } + def make_gui_style(command: Boolean = false): String = + HTML.background_property( + if (command) view.getTextArea.getPainter.getMultipleSelectionColor + else view.getTextArea.getPainter.getSelectionColor) class Renderer extends ListView.Renderer[Entry] { + private object component extends Label { + opaque = false + xAlignment = Alignment.Leading + border = BorderFactory.createEmptyBorder(2, 2, 2, 2) + } + def componentFor( list: ListView[_ <: Timing_Dockable.this.Entry], isSelected: Boolean, focused: Boolean, - entry: Entry, index: Int + entry: Entry, + index: Int ): Component = { - val component = Renderer_Component - component.entry = entry - component.text = entry.print + component.text = entry.gui_text component } } } private abstract class Entry { + def depth: Int = 0 def timing: Double - def print: String + def gui_style: String = "" + def gui_name: GUI.Name + def gui_text: String = { + val style = GUI.Style_HTML + val bullet = if (depth == 0) style.triangular_bullet else style.regular_bullet + style.enclose_style(gui_style, + style.spaces(4 * depth) + bullet + " " + + style.make_text(Time.print_seconds(timing) + "s ") + + gui_name.set_style(style).toString) + } def follow(snapshot: Document.Snapshot): Unit } - private case class Theory_Entry(name: Document.Node.Name, timing: Double, current: Boolean) + private case class Theory_Entry(name: Document.Node.Name, timing: Double) extends Entry { - def print: String = - Time.print_seconds(timing) + "s theory " + quote(name.theory) + def make_current: Theory_Entry = + new Theory_Entry(name, timing) { override val gui_style: String = Entry.make_gui_style() } + def gui_name: GUI.Name = GUI.Name(name.theory, kind = "theory") def follow(snapshot: Document.Snapshot): Unit = PIDE.editor.goto_file(true, view, name.node) } - private case class Command_Entry(command: Command, timing: Double) - extends Entry { - def print: String = - " " + Time.print_seconds(timing) + "s command " + quote(command.span.name) + private case class Command_Entry(command: Command, timing: Double) extends Entry { + override def depth: Int = 1 + override val gui_style: String = Entry.make_gui_style(command = true) + def gui_name: GUI.Name = GUI.Name(command.span.name, kind = "command") def follow(snapshot: Document.Snapshot): Unit = PIDE.editor.hyperlink_command(true, snapshot, command.id).foreach(_.follow(view)) } @@ -133,8 +125,7 @@ handle_update() } tooltip = threshold_tooltip - verifier = ((s: String) => - s match { case Value.Double(x) => x >= 0.0 case _ => false }) + verifier = { case Value.Double(x) => x >= 0.0 case _ => false } } private val controls = Wrap_Panel(List(threshold_label, threshold_value)) @@ -158,13 +149,13 @@ val theories = (for ((node_name, node_timing) <- nodes_timing.toList if node_timing.command_timings.nonEmpty) - yield Theory_Entry(node_name, node_timing.total, false)).sorted(Entry.Ordering) + yield Theory_Entry(node_name, node_timing.total)).sorted(Entry.Ordering) val commands = (for ((command, command_timing) <- timing.command_timings.toList) yield Command_Entry(command, command_timing)).sorted(Entry.Ordering) theories.flatMap(entry => - if (entry.name == name) entry.copy(current = true) :: commands + if (entry.name == name) entry.make_current :: commands else List(entry)) }