# HG changeset patch
# User wenzelm
# Date 1735325385 -3600
# Node ID 70d2f72098df74a3781d46fd7ba60d652ba4c4b9
# Parent  68a9ada23bf85773406c351df2301496fd411ca8
proper bullet symbols for GUI text -- in contrast to Isabelle \<bullet> 0x002219;

diff -r 68a9ada23bf8 -r 70d2f72098df Admin/components/components.sha1
--- a/Admin/components/components.sha1	Fri Dec 27 18:01:34 2024 +0100
+++ b/Admin/components/components.sha1	Fri Dec 27 19:49:45 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 68a9ada23bf8 -r 70d2f72098df Admin/components/main
--- a/Admin/components/main	Fri Dec 27 18:01:34 2024 +0100
+++ b/Admin/components/main	Fri Dec 27 19:49:45 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 68a9ada23bf8 -r 70d2f72098df src/Pure/Admin/component_fonts.scala
--- a/src/Pure/Admin/component_fonts.scala	Fri Dec 27 18:01:34 2024 +0100
+++ b/src/Pure/Admin/component_fonts.scala	Fri Dec 27 19:49:45 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 68a9ada23bf8 -r 70d2f72098df src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Fri Dec 27 18:01:34 2024 +0100
+++ b/src/Pure/GUI/gui.scala	Fri Dec 27 19:49:45 2024 +0100
@@ -102,8 +102,8 @@
         }
       }
 
-    def bullet: String = "\u2218"
-    def bullet_triangle: String = "\u25b9"
+    def regular_bullet: String = "\u2022"
+    def triangular_bullet: String = "\u2023"
   }
 
   abstract class Style_Symbol extends Style {
diff -r 68a9ada23bf8 -r 70d2f72098df src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Fri Dec 27 18:01:34 2024 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Fri Dec 27 19:49:45 2024 +0100
@@ -60,7 +60,7 @@
     def gui_name: GUI.Name
     def gui_text: String = {
       val style = GUI.Style_HTML
-      val bullet = if (depth == 0) style.bullet_triangle else style.bullet
+      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 ") +