# HG changeset patch
# User wenzelm
# Date 1731068846 -3600
# Node ID f92ea68473f2530c118f8fff0c10ddf29698bbb3
# Parent  9f46260073c8392f63cf171f6c1249db9b873978
clarified signature with subtle change of semantics: output consists of individual messages that are formatted (and separated) internally;

diff -r 9f46260073c8 -r f92ea68473f2 src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala	Thu Nov 07 20:43:25 2024 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Fri Nov 08 13:27:26 2024 +0100
@@ -82,8 +82,11 @@
           case Some(node) =>
             graphview.model.full_graph.get_node(node) match {
               case Nil => null
-              case content =>
-                graphview.make_tooltip(graph_pane.peer, event.getX, event.getY, content)
+              case List(tip: XML.Elem) =>
+                graphview.make_tooltip(graph_pane.peer, event.getX, event.getY, tip)
+              case body =>
+                val tip = Pretty.block(body, indent = 0)
+                graphview.make_tooltip(graph_pane.peer, event.getX, event.getY, tip)
             }
           case None => null
         }
diff -r 9f46260073c8 -r f92ea68473f2 src/Tools/Graphview/graphview.scala
--- a/src/Tools/Graphview/graphview.scala	Thu Nov 07 20:43:25 2024 +0100
+++ b/src/Tools/Graphview/graphview.scala	Fri Nov 08 13:27:26 2024 +0100
@@ -85,7 +85,7 @@
 
   /* tooltips */
 
-  def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null
+  def make_tooltip(parent: JComponent, x: Int, y: Int, tip: XML.Elem): String = null
 
 
   /* main colors */
diff -r 9f46260073c8 -r f92ea68473f2 src/Tools/VSCode/src/pretty_text_panel.scala
--- a/src/Tools/VSCode/src/pretty_text_panel.scala	Thu Nov 07 20:43:25 2024 +0100
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala	Fri Nov 08 13:27:26 2024 +0100
@@ -21,14 +21,14 @@
 class Pretty_Text_Panel private(
   resources: VSCode_Resources,
   channel: Channel,
-  output: (String, Option[LSP.Decoration]) => JSON.T
+  output_json: (String, Option[LSP.Decoration]) => JSON.T
 ) {
-  private var current_body: XML.Body = Nil
+  private var current_output: List[XML.Elem] = Nil
   private var current_formatted: XML.Body = Nil
   private var margin: Double = resources.message_margin
 
   private val delay_margin = Delay.last(resources.output_delay, channel.Error_Logger) {
-    refresh(current_body)
+    refresh(current_output)
   }
   
   def update_margin(new_margin: Double): Unit = {
@@ -36,12 +36,13 @@
     delay_margin.invoke()
   }
 
-  def refresh(body: XML.Body): Unit = {
-    val formatted = Pretty.formatted(Pretty.separate(body), margin = margin, metric = Symbol.Metric)
+  def refresh(output: List[XML.Elem]): Unit = {
+    val formatted =
+      Pretty.formatted(Pretty.separate(output), margin = margin, metric = Symbol.Metric)
 
     if (formatted == current_formatted) return
 
-    current_body = body
+    current_output = output
     current_formatted = formatted
 
     if (resources.html_output) {
@@ -57,7 +58,7 @@
         }
       val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full)
       val html = node_context.make_html(elements, formatted)
-      val message = output(HTML.source(html).toString, None)
+      val message = output_json(HTML.source(html).toString, None)
       channel.write(message)
     } else {
       def convert_symbols(body: XML.Body): XML.Body = {
@@ -83,8 +84,7 @@
         })
         .groupMap(_._2)(e => LSP.Decoration_Options(e._1, List())).toList
 
-      val message = output(text, Some(LSP.Decoration(decorations)))
-      channel.write(message)
+      channel.write(output_json(text, Some(LSP.Decoration(decorations))))
     }
   }
 }
diff -r 9f46260073c8 -r f92ea68473f2 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Thu Nov 07 20:43:25 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Fri Nov 08 13:27:26 2024 +0100
@@ -75,7 +75,7 @@
         if (new_threads != current_threads) update_tree(new_threads)
 
         if (new_output != current_output) {
-          pretty_text_area.update(new_snapshot, Command.Results.empty, Pretty.separate(new_output))
+          pretty_text_area.update(new_snapshot, Command.Results.empty, new_output)
         }
 
         current_snapshot = new_snapshot
diff -r 9f46260073c8 -r f92ea68473f2 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Thu Nov 07 20:43:25 2024 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Fri Nov 08 13:27:26 2024 +0100
@@ -71,8 +71,7 @@
   private def show_state(): Unit = GUI_Thread.later {
     val st = current_state.value
 
-    pretty_text_area.update(Document.Snapshot.init, st.output_results,
-      Pretty.separate(st.output_all))
+    pretty_text_area.update(Document.Snapshot.init, st.output_results, st.output_all)
 
     if (st.running) process_indicator.update("Running document build process ...", 15)
     else if (st.pending) process_indicator.update("Waiting for pending document content ...", 5)
diff -r 9f46260073c8 -r f92ea68473f2 src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Thu Nov 07 20:43:25 2024 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Fri Nov 08 13:27:26 2024 +0100
@@ -84,13 +84,13 @@
         val graphview = new isabelle.graphview.Graphview(graph) {
           def options: Options = PIDE.options.value
 
-          override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = {
+          override def make_tooltip(parent: JComponent, x: Int, y: Int, tip: XML.Elem): String = {
             Pretty_Tooltip.invoke(() =>
               {
                 val model = File_Model.init(PIDE.session)
                 val rendering = JEdit_Rendering(snapshot, model, options)
-                val info = Text.Info(Text.Range.offside, body)
-                Pretty_Tooltip(view, parent, new Point(x, y), rendering, Command.Results.empty, info)
+                val loc = new Point(x, y)
+                Pretty_Tooltip(view, parent, loc, rendering, Command.Results.empty, List(tip))
               })
             null
           }
diff -r 9f46260073c8 -r f92ea68473f2 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Thu Nov 07 20:43:25 2024 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala	Fri Nov 08 13:27:26 2024 +0100
@@ -20,12 +20,12 @@
 
   private var implicit_snapshot = Document.Snapshot.init
   private var implicit_results = Command.Results.empty
-  private var implicit_info: XML.Body = Nil
+  private var implicit_info: List[XML.Elem] = Nil
 
   private def set_implicit(
     snapshot: Document.Snapshot,
     results: Command.Results,
-    info: XML.Body
+    info: List[XML.Elem]
   ): Unit = {
     GUI_Thread.require {}
 
@@ -41,7 +41,7 @@
     view: View,
     snapshot: Document.Snapshot,
     results: Command.Results,
-    info: XML.Body
+    info: List[XML.Elem]
   ): Unit = {
     set_implicit(snapshot, results, info)
     view.getDockableWindowManager.floatDockableWindow("isabelle-info")
diff -r 9f46260073c8 -r f92ea68473f2 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Thu Nov 07 20:43:25 2024 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Fri Nov 08 13:27:26 2024 +0100
@@ -542,7 +542,7 @@
     } {
       val loc = new Point(loc0.x, loc0.y + painter.getLineHeight * 3 / 4)
       val results = rendering.snapshot.command_results(tip.range)
-      Pretty_Tooltip(view, painter, loc, rendering, results, tip)
+      Pretty_Tooltip(view, painter, loc, rendering, results, tip.info)
     }
   }
 
diff -r 9f46260073c8 -r f92ea68473f2 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Thu Nov 07 20:43:25 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Fri Nov 08 13:27:26 2024 +0100
@@ -309,10 +309,9 @@
   def tooltip_margin: Int = options.int("jedit_tooltip_margin")
   override def timing_threshold: Double = options.real("jedit_timing_threshold")
 
-  def tooltip(range: Text.Range, control: Boolean): Option[Text.Info[XML.Body]] = {
-    val elements = if (control) Rendering.tooltip_elements else Rendering.tooltip_message_elements
-    tooltips(elements, range).map(info => info.map(Pretty.fbreaks))
-  }
+  def tooltip(range: Text.Range, control: Boolean): Option[Text.Info[List[XML.Elem]]] =
+    tooltips(if (control) Rendering.tooltip_elements else Rendering.tooltip_message_elements,
+      range)
 
   lazy val tooltip_close_icon: Icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
   lazy val tooltip_detach_icon: Icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
diff -r 9f46260073c8 -r f92ea68473f2 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Thu Nov 07 20:43:25 2024 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Nov 08 13:27:26 2024 +0100
@@ -19,7 +19,7 @@
   /* component state -- owned by GUI thread */
 
   private var do_update = true
-  private var current_output: List[XML.Tree] = Nil
+  private var current_output: List[XML.Elem] = Nil
 
 
   /* pretty text area */
@@ -51,7 +51,7 @@
         else current_output
 
       if (current_output != new_output) {
-        pretty_text_area.update(snapshot, results, Pretty.separate(new_output))
+        pretty_text_area.update(snapshot, results, new_output)
         current_output = new_output
       }
     }
diff -r 9f46260073c8 -r f92ea68473f2 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 07 20:43:25 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Nov 08 13:27:26 2024 +0100
@@ -37,7 +37,7 @@
   GUI_Thread.require {}
 
   private var current_font_info: Font_Info = Font_Info.main()
-  private var current_body: XML.Body = Nil
+  private var current_output: List[XML.Elem] = Nil
   private var current_base_snapshot = Document.Snapshot.init
   private var current_base_results = Command.Results.empty
   private var current_rendering: JEdit_Rendering =
@@ -92,13 +92,14 @@
 
       val snapshot = current_base_snapshot
       val results = current_base_results
-      val formatted_body = Pretty.formatted(current_body, margin = margin, metric = metric)
+      val formatted =
+        Pretty.formatted(Pretty.separate(current_output), margin = margin, metric = metric)
 
       future_refresh.foreach(_.cancel())
       future_refresh =
         Some(Future.fork {
           val (text, rendering) =
-            try { JEdit_Rendering.text(snapshot, formatted_body, results = results) }
+            try { JEdit_Rendering.text(snapshot, formatted, results = results) }
             catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
           Exn.Interrupt.expose()
 
@@ -123,24 +124,24 @@
   def update(
     base_snapshot: Document.Snapshot,
     base_results: Command.Results,
-    body: XML.Body
+    output: List[XML.Elem]
   ): Unit = {
     GUI_Thread.require {}
     require(!base_snapshot.is_outdated, "document snapshot outdated")
 
     current_base_snapshot = base_snapshot
     current_base_results = base_results
-    current_body = body
+    current_output = output
     refresh()
   }
 
   def detach(): Unit = {
     GUI_Thread.require {}
-    Info_Dockable(view, current_base_snapshot, current_base_results, current_body)
+    Info_Dockable(view, current_base_snapshot, current_base_results, current_output)
   }
 
   def detach_operation: Option[() => Unit] =
-    if (current_body.isEmpty) None else Some(() => detach())
+    if (current_output.isEmpty) None else Some(() => detach())
 
 
   /* search */
diff -r 9f46260073c8 -r f92ea68473f2 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Thu Nov 07 20:43:25 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Nov 08 13:27:26 2024 +0100
@@ -45,12 +45,12 @@
     location: Point,
     rendering: JEdit_Rendering,
     results: Command.Results,
-    info: Text.Info[XML.Body]
+    output: List[XML.Elem]
   ): Unit = {
     GUI_Thread.require {}
 
     stack match {
-      case top :: _ if top.results == results && top.info == info =>
+      case top :: _ if top.results == results && top.output == output =>
       case _ =>
         GUI.layered_pane(parent) match {
           case None =>
@@ -63,7 +63,7 @@
             old.foreach(_.hide_popup())
 
             val loc = SwingUtilities.convertPoint(parent, location, layered)
-            val tip = new Pretty_Tooltip(view, layered, parent, loc, rendering, results, info)
+            val tip = new Pretty_Tooltip(view, layered, parent, loc, rendering, results, output)
             stack = tip :: rest
             tip.show_popup()
         }
@@ -164,7 +164,7 @@
   location: Point,
   rendering: JEdit_Rendering,
   private val results: Command.Results,
-  private val info: Text.Info[XML.Body]
+  private val output: List[XML.Elem]
 ) extends JPanel(new BorderLayout) {
   tip =>
 
@@ -186,7 +186,7 @@
     listenTo(mouse.clicks)
     reactions += {
       case _: MouseClicked =>
-        Info_Dockable(view, rendering.snapshot, results, info.info)
+        Info_Dockable(view, rendering.snapshot, results, output)
         Pretty_Tooltip.dismiss(tip)
     }
   }
@@ -249,7 +249,7 @@
         ((rendering.tooltip_margin * metric.average) min
           ((w_max - geometry.deco_width) / metric.unit).toInt) max 20
 
-      val formatted = Pretty.formatted(info.info, margin = margin, metric = metric)
+      val formatted = Pretty.formatted(Pretty.separate(output), margin = margin, metric = metric)
       val lines = XML.content_lines(formatted)
 
       val h = painter.getLineHeight * lines + geometry.deco_height
@@ -268,7 +268,7 @@
   private def show_popup(): Unit = {
     popup.show
     pretty_text_area.requestFocus()
-    pretty_text_area.update(rendering.snapshot, results, info.info)
+    pretty_text_area.update(rendering.snapshot, results, output)
   }
 
   private def hide_popup(): Unit = popup.hide
diff -r 9f46260073c8 -r f92ea68473f2 src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Thu Nov 07 20:43:25 2024 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala	Fri Nov 08 13:27:26 2024 +0100
@@ -77,9 +77,7 @@
 
     val query_operation =
       new Query_Operation(PIDE.editor, view, "find_theorems",
-        consume_status(process_indicator, _),
-        (snapshot, results, output) =>
-          pretty_text_area.update(snapshot, results, Pretty.separate(output)))
+        consume_status(process_indicator, _), pretty_text_area.update)
 
     private def apply_query(): Unit = {
       query.addCurrentToHistory()
@@ -140,9 +138,7 @@
 
     val query_operation =
       new Query_Operation(PIDE.editor, view, "find_consts",
-        consume_status(process_indicator, _),
-        (snapshot, results, output) =>
-          pretty_text_area.update(snapshot, results, Pretty.separate(output)))
+        consume_status(process_indicator, _), pretty_text_area.update)
 
     private val query_label = new Label("Find:") {
       tooltip = GUI.tooltip_lines("Name / type patterns for constants")
@@ -217,9 +213,7 @@
 
     val query_operation =
       new Query_Operation(PIDE.editor, view, "print_operation",
-        consume_status(process_indicator, _),
-        (snapshot, results, output) =>
-          pretty_text_area.update(snapshot, results, Pretty.separate(output)))
+        consume_status(process_indicator, _), pretty_text_area.update)
 
     private def apply_query(): Unit =
       query_operation.apply_query(selected_items())
diff -r 9f46260073c8 -r f92ea68473f2 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Nov 07 20:43:25 2024 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Nov 08 13:27:26 2024 +0100
@@ -299,7 +299,7 @@
                           val painter = text_area.getPainter
                           val loc = new Point(x, y + painter.getLineHeight / 2)
                           val results = snapshot.command_results(tip.range)
-                          Pretty_Tooltip(view, painter, loc, rendering, results, tip)
+                          Pretty_Tooltip(view, painter, loc, rendering, results, tip.info)
                       }
                   }
                 }
diff -r 9f46260073c8 -r f92ea68473f2 src/Tools/jEdit/src/simplifier_trace_dockable.scala
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Thu Nov 07 20:43:25 2024 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Fri Nov 08 13:27:26 2024 +0100
@@ -41,8 +41,8 @@
     context.questions.values.toList match {
       case q :: _ =>
         val data = q.data
-        val content = Pretty.separate(XML.Text(data.text) :: data.content)
-        pretty_text_area.update(snapshot, Command.Results.empty, content)
+        val output = List(Pretty.block(XML.Text(data.text) :: data.content, indent = 0))
+        pretty_text_area.update(snapshot, Command.Results.empty, output)
         q.answers.foreach { answer =>
           answers.contents += new GUI.Button(answer.string) {
             override def clicked(): Unit =
diff -r 9f46260073c8 -r f92ea68473f2 src/Tools/jEdit/src/simplifier_trace_window.scala
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Thu Nov 07 20:43:25 2024 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Fri Nov 08 13:27:26 2024 +0100
@@ -56,7 +56,7 @@
     private def body_contains(regex: Regex, body: XML.Body): Boolean =
       body.exists(tree => regex.findFirstIn(XML.content(tree)).isDefined)
 
-    def format: Option[XML.Tree] = {
+    def format: Option[XML.Elem] = {
       def format_hint(data: Simplifier_Trace.Item.Data): XML.Tree =
         Pretty.block(Pretty.separate(XML.Text(data.text) :: data.content))
 
@@ -151,7 +151,7 @@
 
   def handle_update(): Unit = {
     val output = tree.tree_children.flatMap(_.format)
-    pretty_text_area.update(snapshot, Command.Results.empty, Pretty.separate(output))
+    pretty_text_area.update(snapshot, Command.Results.empty, output)
   }
 
   def handle_resize(): Unit = pretty_text_area.zoom()
diff -r 9f46260073c8 -r f92ea68473f2 src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Thu Nov 07 20:43:25 2024 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Nov 08 13:27:26 2024 +0100
@@ -46,9 +46,7 @@
   }
 
   private val sledgehammer =
-    new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status,
-      (snapshot, results, output) =>
-        pretty_text_area.update(snapshot, results, Pretty.separate(output)))
+    new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status, pretty_text_area.update)
 
 
   /* resize */
diff -r 9f46260073c8 -r f92ea68473f2 src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala	Thu Nov 07 20:43:25 2024 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala	Fri Nov 08 13:27:26 2024 +0100
@@ -27,9 +27,7 @@
   override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
 
   private val print_state =
-    new Query_Operation(PIDE.editor, view, "print_state", _ => (),
-      (snapshot, results, output) =>
-        pretty_text_area.update(snapshot, results, Pretty.separate(output)))
+    new Query_Operation(PIDE.editor, view, "print_state", _ => (), pretty_text_area.update)
 
 
   /* resize */