Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified signature;
authorwenzelm
Thu, 07 Nov 2024 20:08:50 +0100
changeset 81394 95b53559af80
parent 81393 4ee8da9e48ea
child 81395 d9f791f75b8b
clarified signature;
src/Pure/PIDE/query_operation.scala file | annotate | diff | comparison | revisions
src/Tools/VSCode/src/state_panel.scala file | annotate | diff | comparison | revisions
src/Tools/jEdit/src/query_dockable.scala file | annotate | diff | comparison | revisions
src/Tools/jEdit/src/sledgehammer_dockable.scala file | annotate | diff | comparison | revisions
src/Tools/jEdit/src/state_dockable.scala file | annotate | diff | comparison | revisions 
--- 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"
 
--- 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()
--- 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())
--- 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 */
--- 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 */
isabelle