# HG changeset patch
# User wenzelm
# Date 1731006530 -3600
# Node ID 95b53559af80885bc8baf2bfb85af328d6963d91
# Parent  4ee8da9e48ea85d25c6dbc73fca8e7db1107ab5a
clarified signature;

diff -r 4ee8da9e48ea -r 95b53559af80 src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Thu Nov 07 20:02:10 2024 +0100
+++ b/src/Pure/PIDE/query_operation.scala	Thu Nov 07 20:08:50 2024 +0100
@@ -36,7 +36,7 @@
   editor_context: Editor_Context,
   operation_name: String,
   consume_status: Query_Operation.Status => Unit,
-  consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit
+  consume_output: (Document.Snapshot, Command.Results, List[XML.Elem]) => Unit
 ) {
   private val print_function = operation_name + "_query"
 
diff -r 4ee8da9e48ea -r 95b53559af80 src/Tools/VSCode/src/state_panel.scala
--- a/src/Tools/VSCode/src/state_panel.scala	Thu Nov 07 20:02:10 2024 +0100
+++ b/src/Tools/VSCode/src/state_panel.scala	Thu Nov 07 20:08:50 2024 +0100
@@ -70,9 +70,9 @@
 
   private val print_state =
     new Query_Operation(server.editor, (), "print_state", _ => (),
-      (_, _, body) =>
-        if (output_active.value && body.nonEmpty) {
-          pretty_panel.value.refresh(body)
+      (_, _, output) =>
+        if (output_active.value && output.nonEmpty) {
+          pretty_panel.value.refresh(output)
         })
 
   def locate(): Unit = print_state.locate_query()
diff -r 4ee8da9e48ea -r 95b53559af80 src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Thu Nov 07 20:02:10 2024 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala	Thu Nov 07 20:08:50 2024 +0100
@@ -78,8 +78,8 @@
     val query_operation =
       new Query_Operation(PIDE.editor, view, "find_theorems",
         consume_status(process_indicator, _),
-        (snapshot, results, body) =>
-          pretty_text_area.update(snapshot, results, Pretty.separate(body)))
+        (snapshot, results, output) =>
+          pretty_text_area.update(snapshot, results, Pretty.separate(output)))
 
     private def apply_query(): Unit = {
       query.addCurrentToHistory()
@@ -141,8 +141,8 @@
     val query_operation =
       new Query_Operation(PIDE.editor, view, "find_consts",
         consume_status(process_indicator, _),
-        (snapshot, results, body) =>
-          pretty_text_area.update(snapshot, results, Pretty.separate(body)))
+        (snapshot, results, output) =>
+          pretty_text_area.update(snapshot, results, Pretty.separate(output)))
 
     private val query_label = new Label("Find:") {
       tooltip = GUI.tooltip_lines("Name / type patterns for constants")
@@ -218,8 +218,8 @@
     val query_operation =
       new Query_Operation(PIDE.editor, view, "print_operation",
         consume_status(process_indicator, _),
-        (snapshot, results, body) =>
-          pretty_text_area.update(snapshot, results, Pretty.separate(body)))
+        (snapshot, results, output) =>
+          pretty_text_area.update(snapshot, results, Pretty.separate(output)))
 
     private def apply_query(): Unit =
       query_operation.apply_query(selected_items())
diff -r 4ee8da9e48ea -r 95b53559af80 src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Thu Nov 07 20:02:10 2024 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Thu Nov 07 20:08:50 2024 +0100
@@ -47,8 +47,8 @@
 
   private val sledgehammer =
     new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status,
-      (snapshot, results, body) =>
-        pretty_text_area.update(snapshot, results, Pretty.separate(body)))
+      (snapshot, results, output) =>
+        pretty_text_area.update(snapshot, results, Pretty.separate(output)))
 
 
   /* resize */
diff -r 4ee8da9e48ea -r 95b53559af80 src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala	Thu Nov 07 20:02:10 2024 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala	Thu Nov 07 20:08:50 2024 +0100
@@ -28,8 +28,8 @@
 
   private val print_state =
     new Query_Operation(PIDE.editor, view, "print_state", _ => (),
-      (snapshot, results, body) =>
-        pretty_text_area.update(snapshot, results, Pretty.separate(body)))
+      (snapshot, results, output) =>
+        pretty_text_area.update(snapshot, results, Pretty.separate(output)))
 
 
   /* resize */