# HG changeset patch
# User wenzelm
# Date 1667378847 -3600
# Node ID fb9c567a67cd0d9a949a5c27c1112894c9fc4f96
# Parent  d9c78a18b44b240b9f8811de8c216665556742df
clarified modules;

diff -r d9c78a18b44b -r fb9c567a67cd src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Mon Oct 31 21:58:08 2022 +0100
+++ b/src/Pure/PIDE/command.ML	Wed Nov 02 09:47:27 2022 +0100
@@ -419,25 +419,6 @@
 
 end;
 
-val _ =
-  print_function "Execution.print"
-    (fn {args, exec_id, ...} =>
-      if null args then
-        SOME {delay = NONE, pri = Task_Queue.urgent_pri + 2, persistent = false, strict = false,
-          print_fn = fn _ => fn _ => Execution.fork_prints exec_id}
-      else NONE);
-
-val _ =
-  print_function "print_state"
-    (fn {keywords, command_name, ...} =>
-      if Options.default_bool "editor_output_state" andalso Keyword.is_printed keywords command_name
-      then
-        SOME {delay = NONE, pri = Task_Queue.urgent_pri + 1, persistent = false, strict = false,
-          print_fn = fn _ => fn st =>
-            if Toplevel.is_proof st then Output.state (Toplevel.string_of_state st)
-            else ()}
-      else NONE);
-
 
 (* combined execution *)
 
@@ -502,3 +483,25 @@
 end;
 
 end;
+
+
+(* common print functions *)
+
+val _ =
+  Command.print_function "Execution.print"
+    (fn {args, exec_id, ...} =>
+      if null args then
+        SOME {delay = NONE, pri = Task_Queue.urgent_pri + 2, persistent = false, strict = false,
+          print_fn = fn _ => fn _ => Execution.fork_prints exec_id}
+      else NONE);
+
+val _ =
+  Command.print_function "print_state"
+    (fn {keywords, command_name, ...} =>
+      if Options.default_bool "editor_output_state" andalso Keyword.is_printed keywords command_name
+      then
+        SOME {delay = NONE, pri = Task_Queue.urgent_pri + 1, persistent = false, strict = false,
+          print_fn = fn _ => fn st =>
+            if Toplevel.is_proof st then Output.state (Toplevel.string_of_state st)
+            else ()}
+      else NONE);
diff -r d9c78a18b44b -r fb9c567a67cd src/Pure/PIDE/query_operation.ML
--- a/src/Pure/PIDE/query_operation.ML	Mon Oct 31 21:58:08 2022 +0100
+++ b/src/Pure/PIDE/query_operation.ML	Wed Nov 02 09:47:27 2022 +0100
@@ -39,14 +39,13 @@
           in () end)}
     | _ => NONE);
 
+end;
 
 (* print_state *)
 
 val _ =
-  register {name = "print_state", pri = Task_Queue.urgent_pri}
+  Query_Operation.register {name = "print_state", pri = Task_Queue.urgent_pri}
     (fn {state = st, output_result, ...} =>
       if Toplevel.is_proof st
       then output_result (Markup.markup Markup.state (Toplevel.string_of_state st))
       else ());
-
-end;
diff -r d9c78a18b44b -r fb9c567a67cd src/Pure/Tools/print_operation.ML
--- a/src/Pure/Tools/print_operation.ML	Mon Oct 31 21:58:08 2022 +0100
+++ b/src/Pure/Tools/print_operation.ML	Wed Nov 02 09:47:27 2022 +0100
@@ -52,22 +52,23 @@
 
 end;
 
+end;
+
 
 (* common print operations *)
 
 val _ =
-  register "context" "context of local theory target" Toplevel.pretty_context;
+  Print_Operation.register "context" "context of local theory target"
+    Toplevel.pretty_context;
 
 val _ =
-  register "cases" "cases of proof context"
+  Print_Operation.register "cases" "cases of proof context"
     (Proof_Context.pretty_cases o Toplevel.context_of);
 
 val _ =
-  register "terms" "term bindings of proof context"
+  Print_Operation.register "terms" "term bindings of proof context"
     (Proof_Context.pretty_term_bindings o Toplevel.context_of);
 
 val _ =
-  register "theorems" "theorems of local theory or proof context"
+  Print_Operation.register "theorems" "theorems of local theory or proof context"
     (Isar_Cmd.pretty_theorems false);
-
-end;