# HG changeset patch
# User wenzelm
# Date 1691947678 -7200
# Node ID 3d6dbf215559bc597a94c9745dd4e071010cc36a
# Parent  374611eb30550d3f9a0035eeaf0d5f38fcc60c53
clarified command arguments: optionally restrict to given theories (from theory loader);

diff -r 374611eb3055 -r 3d6dbf215559 NEWS
--- a/NEWS	Sun Aug 13 19:23:53 2023 +0200
+++ b/NEWS	Sun Aug 13 19:27:58 2023 +0200
@@ -423,11 +423,10 @@
   isabelle process -l ZF -e "Session.print_context_tracing (K true)"
 
 An alternative to "isabelle process -l ZF" is "isabelle jedit -l ZF"
-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>
+with the subsequent Isar commands:
+
+  print_context_tracing
+  print_context_tracing ZF.Nat ZF.Int  \<comment> \<open>restriction to theories\<close>
 
 * The "rsync" tool has been bundled as Isabelle component, with uniform
 version and compilation options on all platforms. This allows to use
diff -r 374611eb3055 -r 3d6dbf215559 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sun Aug 13 19:23:53 2023 +0200
+++ b/src/Pure/Pure.thy	Sun Aug 13 19:27:58 2023 +0200
@@ -1301,7 +1301,17 @@
 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))));
+    (Scan.repeat Parse.name_position >> (fn raw_names => Toplevel.keep (fn st =>
+      let
+        val pred =
+          if null raw_names then K true
+          else
+            let
+              val ctxt = Toplevel.context_of st;
+              val insert = Symset.insert o Context.theory_long_name o Thy_Info.check_theory ctxt;
+              val names = Symset.build (fold insert raw_names);
+            in Symset.member names o Context.theory_long_name o Context.theory_of end;
+      in Session.print_context_tracing pred end)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_state\<close>