--- 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
--- 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
--- 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:
- "(\<And>x. Rep_fin_defl a\<cdot>x = x \<longleftrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a = b"
-apply (rule below_antisym)
-apply (rule fin_defl_belowI, simp)
-apply (rule fin_defl_belowI, simp)
-done
+ "a = b" if "(\<And>x. Rep_fin_defl a\<cdot>x = x \<longleftrightarrow> Rep_fin_defl b\<cdot>x = x)"
+proof (rule below_antisym)
+ show "a \<sqsubseteq> b" by (rule fin_defl_belowI) (simp add: that)
+ show "b \<sqsubseteq> a" by (rule fin_defl_belowI) (simp add: that)
+qed
lemma Rep_fin_defl_mono: "a \<sqsubseteq> b \<Longrightarrow> Rep_fin_defl a \<sqsubseteq> 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 "\<And>x. compact x \<Longrightarrow> d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
-by (rule belowI, rule assms, erule subst, rule compact)
+ "d \<sqsubseteq> f" if "\<And>x. compact x \<Longrightarrow> d\<cdot>x = x \<Longrightarrow> f\<cdot>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 \<sqsubseteq> y \<longleftrightarrow> Rep_defl x \<subseteq> Rep_defl y"
+definition "x \<sqsubseteq> y \<longleftrightarrow> Rep_defl x \<subseteq> 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 \<Rightarrow> 'a defl" where
- "defl_principal t = Abs_defl {u. u \<sqsubseteq> t}"
+definition defl_principal :: "'a::bifinite fin_defl \<Rightarrow> 'a defl"
+ where "defl_principal t = Abs_defl {u. u \<sqsubseteq> t}"
lemma fin_defl_countable: "\<exists>f::'a::bifinite fin_defl \<Rightarrow> nat. inj f"
proof -
@@ -134,11 +133,13 @@
text \<open>Algebraic deflations are pointed\<close>
lemma defl_minimal: "defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> 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 \<bottom> \<sqsubseteq> a"
+ by (simp add: below_fin_defl_def Abs_fin_defl_inverse finite_deflation_bottom)
+ then show "defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> 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 \<open>Applying algebraic deflations\<close>
-definition
- cast :: "'a::bifinite defl \<rightarrow> 'a \<rightarrow> 'a"
-where
- "cast = defl.extension Rep_fin_defl"
+definition cast :: "'a::bifinite defl \<rightarrow> 'a \<rightarrow> 'a"
+ where "cast = defl.extension Rep_fin_defl"
-lemma cast_defl_principal:
- "cast\<cdot>(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\<cdot>(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\<cdot>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 \<Longrightarrow> finite_deflation (cast\<cdot>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 \<Longrightarrow> finite_deflation (cast\<cdot>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\<cdot>d"
by (rule deflation_cast)
declare cast.idem [simp]
-lemma compact_cast [simp]: "compact d \<Longrightarrow> compact (cast\<cdot>d)"
-apply (rule finite_deflation_imp_compact)
-apply (erule finite_deflation_cast)
-done
+lemma compact_cast [simp]: "compact (cast\<cdot>d)" if "compact d"
+ by (rule finite_deflation_imp_compact) (use that in \<open>rule finite_deflation_cast\<close>)
lemma cast_below_cast: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<longleftrightarrow> A \<sqsubseteq> B"
apply (induct A rule: defl.principal_induct, simp)
@@ -236,10 +230,13 @@
assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
shows "cast\<cdot>(defl_fun1 e p f\<cdot>A) = e oo f\<cdot>(cast\<cdot>A) oo p"
proof -
- have 1: "\<And>a. finite_deflation (e oo f\<cdot>(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\<cdot>(Rep_fin_defl a) oo p)" for a
+ proof -
+ have "finite_deflation (f\<cdot>(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\<cdot>a\<cdot>b)"
shows "cast\<cdot>(defl_fun2 e p f\<cdot>A\<cdot>B) = e oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo p"
proof -
- have 1: "\<And>a b. finite_deflation
- (e oo f\<cdot>(Rep_fin_defl a)\<cdot>(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\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo p)" for a b
+ proof -
+ have "finite_deflation (f\<cdot>(Rep_fin_defl a)\<cdot>(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)
--- 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
--- 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
--- 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 =>
}
--- 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)
--- 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 = "<b>" + make_text(str) + "</b>"
+ 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 ++= "<html>"
+ s ++= body
+ s ++= "</html>"
+ }
+ }
+ else {
+ Library.string_builder(style.length + body.length + 35) { s =>
+ s ++= "<html><span style=\""
+ s ++= style
+ s ++= "\">"
+ s ++= body
+ s ++= "</span></html>"
+ }
+ }
+
+ 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>" + HTML.output(text) + "</html>"
+ else Style_HTML.enclose_text(text)
/* icon */
--- 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 =
--- 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 */
--- 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
}
--- 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 */
--- 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)
}
--- 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, _), _))) =>
--- 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 => }
--- 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><b>" + HTML.output(name) + "</b>: " + HTML.output(title) + "</html>"
+ val style = GUI.Style_HTML
+ style.enclose(style.make_bold(name) + style.make_text(": " + title))
}
else name
}
--- 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("<html><b>Apply</b></html>") { selection_action () }
+ action = Action(GUI.Style_HTML.enclose_bold("Apply")) { selection_action () }
tooltip = "Apply tree selection to graph"
}
--- 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)) +
- "<b>" + HTML.output(keyword) + "</b>" +
- 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)
}
- "<html><span style=\"" + css + "\">" + s + "</span></html>"
+ 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><b>" + HTML.output(kind) + "</b>" +
- if_proper(name, " " + HTML.output(name)) + "</html>"
+ 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))
--- 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><b>" + HTML.output(Symbol.print_newlines(a)) + "</b>" +
- HTML.output(bs.map(b => " " + Symbol.print_newlines(b)).mkString) + "</html>"
+ 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
--- 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("<html><b>Eval</b></html>") {
+ new GUI.Button(GUI.Style_HTML.enclose_bold("Eval")) {
tooltip = "Evaluate ML expression within optional context"
override def clicked(): Unit = eval_expression()
}
--- 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("<html><b>Build</b></html>") {
+ new GUI.Button(GUI.Style_HTML.enclose_bold("Build")) {
tooltip = "Build document"
override def clicked(): Unit = pending_process()
}
--- 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>" + HTML.output(shortcut.toString) + "</html>"
- else
- "<html><font style='color: #" + Color_Value.print(conflict_color) + ";'>" +
- HTML.output("--- " + shortcut.toString) +
- "</font></html>"
+ 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 {
--- 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 ++= ":</b> "
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 ++= "<span style=\""
s ++= highlight_style
s ++= "\">"
- s ++= plain_text.substring(next, next + range.length)
+ s ++= line_text.substring(next, next + range.length)
s ++= "</span>"
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 ++= "</html>"
}
override def toString: String = gui_text
--- 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("<html><b>Apply</b></html>") {
+ 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("<html><b>Apply</b></html>") {
+ 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("<html><b>Apply</b></html>") {
+ private val apply_button = new GUI.Button(GUI.Style_HTML.enclose_bold("Apply")) {
tooltip = "Apply to current context"
override def clicked(): Unit = apply_query()
--- 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("<html><b>Apply</b></html>") {
+ 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()
}
--- 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("<html><b>Update</b></html>") {
+ 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()
}
--- 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>" + HTML.output(Symbol.decode(txt)) + "</html>"
+ text = GUI.Style_HTML.enclose_text(Symbol.decode(txt))
action =
Action(text) {
val text_area = view.getTextArea
--- 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}
--- 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))
}