# HG changeset patch
# User wenzelm
# Date 1691941831 -7200
# Node ID fd3fa1790a96fd17c11302caa71de44b6d8b2913
# Parent  f5d7ed37f06ae2258dbf3f84683fd1de98f85c75
added Isar command 'print_context_tracing';

diff -r f5d7ed37f06a -r fd3fa1790a96 NEWS
--- 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>
diff -r f5d7ed37f06a -r fd3fa1790a96 src/Pure/Pure.thy
--- 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 =>