src/Pure/Pure.thy

     "print_interps" "print_attributes"
     "print_simpset" "print_rules" "print_trans_rules" "print_methods"
     "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
   and "realizers" :: thy_decl
   and "realizability" :: thy_decl

 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_codesetup\<close> "print code generator setup"
     (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 =>
       Toplevel.keep (Print_Mode.with_modes modes (Output.writeln o Toplevel.string_of_state))));