--- 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);
--- 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;
--- 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;