--- a/NEWS Sun Aug 13 15:06:17 2023 +0200
+++ b/NEWS Sun Aug 13 17:50:31 2023 +0200
@@ -423,7 +423,8 @@
isabelle process -l ZF -e "Session.print_context_tracing (K true)"
An alternative to "isabelle process -l ZF" is "isabelle jedit -l ZF"
-with the subsequent ML snippets in an arbitrary theory context:
+with with the Isar command 'print_context_tracing' or with the
+subsequent ML snippets (in an arbitrary theory context):
ML_command \<open>Session.print_context_tracing (K true)\<close>
ML \<open>Context.finish_tracing ()\<close>
--- a/src/Pure/Pure.thy Sun Aug 13 15:06:17 2023 +0200
+++ b/src/Pure/Pure.thy Sun Aug 13 17:50:31 2023 +0200
@@ -88,7 +88,7 @@
"print_antiquotations" "print_ML_antiquotations" "thy_deps"
"locale_deps" "class_deps" "thm_deps" "thm_oracles" "print_term_bindings"
"print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf"
- "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
+ "prop" "term" "typ" "print_codesetup" "print_context_tracing" "unused_thms" :: diag
and "print_state" :: diag
and "welcome" :: diag
and "end" :: thy_end
@@ -1299,6 +1299,11 @@
(Scan.succeed (Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
val _ =
+ Outer_Syntax.command \<^command_keyword>\<open>print_context_tracing\<close>
+ "print result of context tracing from ML heap"
+ (Scan.succeed (Toplevel.keep (fn _ => Session.print_context_tracing (K true))));
+
+val _ =
Outer_Syntax.command \<^command_keyword>\<open>print_state\<close>
"print current proof state (if present)"
(opt_modes >> (fn modes =>