# HG changeset patch
# User wenzelm
# Date 1735227226 -3600
# Node ID e711873dcb53ebbfaaec238b86f161cc746fedff
# Parent  98ecc0ed6af1a126524e9ee1be5143008eab8ca7
tuned GUI output;

diff -r 98ecc0ed6af1 -r e711873dcb53 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Thu Dec 26 16:16:28 2024 +0100
+++ b/src/Pure/GUI/gui.scala	Thu Dec 26 16:33:46 2024 +0100
@@ -95,7 +95,11 @@
 
   object Style_Plain extends Style { override def toString: String = "plain" }
 
-  object Style_HTML extends Style_HTML { override def toString: String = "html" }
+  object Style_HTML extends Style_HTML {
+    override def toString: String = "html"
+    def bullet: String = "\u2218"
+    def bullet_triangle: String = "\u25b9"
+  }
 
   object Style_Symbol_Encoded extends Style_Symbol {
     override def toString: String = "symbol_encoded"
diff -r 98ecc0ed6af1 -r e711873dcb53 src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Thu Dec 26 16:16:28 2024 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Thu Dec 26 16:33:46 2024 +0100
@@ -78,8 +78,10 @@
     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
       style.enclose(
-        style.spaces(2 * depth) + style.make_text(Time.print_seconds(timing) + "s ") +
+        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