# HG changeset patch
# User wenzelm
# Date 1761575807 -3600
# Node ID 0ac8a8a3793b41a38b06993b315d37287f8843c6
# Parent  a2e6778087657a7240346ab4ba8b2112fd0e8d97
clarified signature: prefer explicit type Editor.Output;

diff -r a2e677808765 -r 0ac8a8a3793b src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Mon Oct 27 15:24:25 2025 +0100
+++ b/src/Pure/PIDE/editor.scala	Mon Oct 27 15:36:47 2025 +0100
@@ -20,7 +20,9 @@
     results: Command.Results = Command.Results.empty,
     messages: List[XML.Elem] = Nil,
     defined: Boolean = true
-  )
+  ) {
+    def proper: Boolean = messages.nonEmpty && defined
+  }
 }
 
 abstract class Editor[Context] {
diff -r a2e677808765 -r 0ac8a8a3793b src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Mon Oct 27 15:24:25 2025 +0100
+++ b/src/Pure/PIDE/query_operation.scala	Mon Oct 27 15:36:47 2025 +0100
@@ -36,7 +36,7 @@
   editor_context: Editor_Context,
   operation_name: String,
   consume_status: Query_Operation.Status => Unit,
-  consume_output: (Document.Snapshot, Command.Results, List[XML.Elem]) => Unit
+  consume_output: Editor.Output => Unit
 ) {
   private val print_function = operation_name + "_query"
 
@@ -150,7 +150,8 @@
         current_state.change(_.copy(update_pending = false))
         if (state0.output != new_output && !removed) {
           current_state.change(_.copy(output = new_output))
-          consume_output(snapshot, command_results, new_output)
+          consume_output(
+            Editor.Output(snapshot = snapshot, results = command_results, messages = new_output))
         }
         if (state0.status != new_status) {
           current_state.change(_.copy(status = new_status))
@@ -175,7 +176,7 @@
       case Some(snapshot) =>
         remove_overlay()
         current_state.change(_ => Query_Operation.State.empty)
-        consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
+        consume_output(Editor.Output.init)
 
         editor.current_command(editor_context, snapshot) match {
           case Some(command) =>
@@ -227,7 +228,7 @@
     editor.session.commands_changed -= main
     remove_overlay()
     current_state.change(_ => Query_Operation.State.empty)
-    consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
+    consume_output(Editor.Output.init)
     consume_status(Query_Operation.Status.finished)
   }
 }
diff -r a2e677808765 -r 0ac8a8a3793b src/Tools/VSCode/src/state_panel.scala
--- a/src/Tools/VSCode/src/state_panel.scala	Mon Oct 27 15:24:25 2025 +0100
+++ b/src/Tools/VSCode/src/state_panel.scala	Mon Oct 27 15:36:47 2025 +0100
@@ -70,9 +70,9 @@
 
   private val print_state =
     new Query_Operation(server.editor, (), "print_state", _ => (),
-      (_, _, output) =>
-        if (output_active.value && output.nonEmpty) {
-          pretty_panel.value.refresh(output)
+      output =>
+        if (output_active.value && output.proper) {
+          pretty_panel.value.refresh(output.messages)
         })
 
   def locate(): Unit = print_state.locate_query()
diff -r a2e677808765 -r 0ac8a8a3793b src/Tools/VSCode/src/vscode_sledgehammer.scala
--- a/src/Tools/VSCode/src/vscode_sledgehammer.scala	Mon Oct 27 15:24:25 2025 +0100
+++ b/src/Tools/VSCode/src/vscode_sledgehammer.scala	Mon Oct 27 15:36:47 2025 +0100
@@ -20,7 +20,7 @@
 
 class VSCode_Sledgehammer private(server: Language_Server) {
   private val query_operation =
-    new Query_Operation(server.editor, (), "sledgehammer", consume_status, consume_result)
+    new Query_Operation(server.editor, (), "sledgehammer", consume_status, consume_output)
 
   private var last_sendback_id: Option[Int] = None
 
@@ -117,11 +117,10 @@
     }
   }
 
-  private def consume_result(
-    snapshot: Document.Snapshot,
-    results: Command.Results,
-    body: List[XML.Elem]
-  ): Unit = {
+  private def consume_output(output: Editor.Output): Unit = {
+    val snapshot = output.snapshot
+    val body = output.messages
+
     val xml_string = body.map(XML.string_of_tree).mkString
 
     if (xml_string.contains("Done")) {
diff -r a2e677808765 -r 0ac8a8a3793b src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Mon Oct 27 15:24:25 2025 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala	Mon Oct 27 15:36:47 2025 +0100
@@ -77,7 +77,7 @@
 
     val query_operation =
       new Query_Operation(PIDE.editor, view, "find_theorems",
-        consume_status(process_indicator, _), pretty_text_area.update)
+        consume_status(process_indicator, _), pretty_text_area.update_output)
 
     private def apply_query(): Unit = {
       query.addCurrentToHistory()
@@ -139,7 +139,7 @@
 
     val query_operation =
       new Query_Operation(PIDE.editor, view, "find_consts",
-        consume_status(process_indicator, _), pretty_text_area.update)
+        consume_status(process_indicator, _), pretty_text_area.update_output)
 
     private val query_label = new Label("Find:") {
       tooltip = GUI.tooltip_lines("Name / type patterns for constants")
@@ -214,7 +214,7 @@
 
     val query_operation =
       new Query_Operation(PIDE.editor, view, "print_operation",
-        consume_status(process_indicator, _), pretty_text_area.update)
+        consume_status(process_indicator, _), pretty_text_area.update_output)
 
     private def apply_query(): Unit =
       query_operation.apply_query(selected_items())
diff -r a2e677808765 -r 0ac8a8a3793b src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Mon Oct 27 15:24:25 2025 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Mon Oct 27 15:36:47 2025 +0100
@@ -51,7 +51,7 @@
 
   private val sledgehammer =
     new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status,
-      output.pretty_text_area.update)
+      output.pretty_text_area.update_output)
 
 
   /* controls */
diff -r a2e677808765 -r 0ac8a8a3793b src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala	Mon Oct 27 15:24:25 2025 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala	Mon Oct 27 15:36:47 2025 +0100
@@ -30,7 +30,8 @@
   override def detach_operation: Option[() => Unit] = output.pretty_text_area.detach_operation
 
   private val print_state =
-    new Query_Operation(PIDE.editor, view, "print_state", _ => (), output.pretty_text_area.update)
+    new Query_Operation(PIDE.editor, view, "print_state", _ => (),
+      output.pretty_text_area.update_output)
 
   output.setup(dockable)
   set_content(output.split_pane)