# HG changeset patch
# User wenzelm
# Date 1025624653 -7200
# Node ID 20c818c966e6575c3d552bb60c158d6452e6272c
# Parent  1051aa66cbf395d4a8dcff4a5aea4409bf58ce91
thms_containing: optional limit argument;

diff -r 1051aa66cbf3 -r 20c818c966e6 NEWS
--- a/NEWS	Tue Jul 02 17:00:05 2002 +0200
+++ b/NEWS	Tue Jul 02 17:44:13 2002 +0200
@@ -9,7 +9,9 @@
 
 * improved thms_containing: proper indexing of facts instead of raw
 theorems; check validity of results wrt. current name space; include
-local facts of proof configuration (also covers active locales);
+local facts of proof configuration (also covers active locales); an
+optional limit for the number of printed facts may be given (the
+default is 40);
 
 
 *** HOL ***
diff -r 1051aa66cbf3 -r 20c818c966e6 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Tue Jul 02 17:00:05 2002 +0200
+++ b/doc-src/IsarRef/pure.tex	Tue Jul 02 17:44:13 2002 +0200
@@ -1355,7 +1355,7 @@
 \railterm{thmdeps}
 
 \begin{rail}
-  thmscontaining (term * )
+  thmscontaining ('(' nat ')')? (term * )
   ;
   thmdeps thmrefs
   ;
@@ -1391,7 +1391,8 @@
 \item [$\isarkeyword{thms_containing}~\vec t$] retrieves facts from the theory
   or proof context containing all of the constants or variables occurring in
   terms $\vec t$.  Note that giving the empty list yields \emph{all} currently
-  known facts.
+  known facts.  An optional limit for the number printed facts may be given;
+  the default is 40.
   
 \item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of facts,
   using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
diff -r 1051aa66cbf3 -r 20c818c966e6 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Jul 02 17:00:05 2002 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Jul 02 17:44:13 2002 +0200
@@ -54,7 +54,8 @@
   val print_trans_rules: Toplevel.transition -> Toplevel.transition
   val print_methods: Toplevel.transition -> Toplevel.transition
   val print_antiquotations: Toplevel.transition -> Toplevel.transition
-  val print_thms_containing: string list -> Toplevel.transition -> Toplevel.transition
+  val print_thms_containing: int option * string list
+    -> Toplevel.transition -> Toplevel.transition
   val thm_deps: (string * Args.src list) list -> Toplevel.transition -> Toplevel.transition
   val print_binds: Toplevel.transition -> Toplevel.transition
   val print_lthms: Toplevel.transition -> Toplevel.transition
@@ -224,9 +225,9 @@
 
 val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations;
 
-fun print_thms_containing ss = Toplevel.unknown_theory o Toplevel.keep (fn state =>
+fun print_thms_containing (lim, spec) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   ProofContext.print_thms_containing
-    (Toplevel.node_case ProofContext.init Proof.context_of state) ss);
+    (Toplevel.node_case ProofContext.init Proof.context_of state) lim spec);
 
 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   ThmDeps.thm_deps (IsarThy.get_thmss args (Toplevel.enter_forward_proof state)));
diff -r 1051aa66cbf3 -r 20c818c966e6 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Jul 02 17:00:05 2002 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jul 02 17:44:13 2002 +0200
@@ -583,7 +583,8 @@
 val thms_containingP =
   OuterSyntax.improper_command "thms_containing"
     "print facts containing certain constants or variables"
-    K.diag (Scan.repeat P.term >> (Toplevel.no_timing oo IsarCmd.print_thms_containing));
+    K.diag (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
+      Scan.repeat P.term >> (Toplevel.no_timing oo IsarCmd.print_thms_containing));
 
 val thm_depsP =
   OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
diff -r 1051aa66cbf3 -r 20c818c966e6 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Jul 02 17:00:05 2002 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Jul 02 17:44:13 2002 +0200
@@ -125,7 +125,8 @@
   val prems_limit: int ref
   val pretty_asms: context -> Pretty.T list
   val pretty_context: context -> Pretty.T list
-  val print_thms_containing: context -> string list -> unit
+  val thms_containing_limit: int ref
+  val print_thms_containing: context -> int option -> string list -> unit
   val setup: (theory -> theory) list
 end;
 
@@ -1378,7 +1379,9 @@
   in gen_distinct eq_fst (filter valid (FactIndex.find idx index)) end;
 
 
-fun print_thms_containing ctxt ss =
+val thms_containing_limit = ref 40;
+
+fun print_thms_containing ctxt opt_limit ss =
   let
     val prt_term = pretty_term ctxt;
     val prt_fact = pretty_fact ctxt;
@@ -1398,13 +1401,16 @@
       else [Pretty.block (Pretty.breaks (Pretty.str "Facts containing" ::
         separate (Pretty.str "and") (prt_consts cs @ prt_frees xs)) @
           [Pretty.str ":", Pretty.fbrk])]
-    val globals = PureThy.thms_containing (theory_of ctxt) (cs, xs);
-    val locals = lthms_containing ctxt (cs, xs);
+    val facts =
+      PureThy.thms_containing (theory_of ctxt) (cs, xs) @ lthms_containing ctxt (cs, xs)
+      |> sort_wrt #1;
+    val len = length facts;
+    val limit = if_none opt_limit (! thms_containing_limit);
   in
     if empty_idx andalso not (Library.null ss) then
       warning "thms_containing: no consts/frees in specification"
-    else (header @ map prt_fact (sort_wrt #1 (globals @ locals)))
-      |> Pretty.chunks |> Pretty.writeln
+    else (header @ (if len <= limit then [] else [Pretty.str "..."]) @
+        map prt_fact (Library.drop (len - limit, facts))) |> Pretty.chunks |> Pretty.writeln
   end;
 
 
diff -r 1051aa66cbf3 -r 20c818c966e6 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Tue Jul 02 17:00:05 2002 +0200
+++ b/src/Pure/proof_general.ML	Tue Jul 02 17:44:13 2002 +0200
@@ -220,7 +220,7 @@
 (* misc commands for ProofGeneral/isa *)
 
 fun thms_containing ss =
-  ProofContext.print_thms_containing (ProofContext.init (the_context ())) ss;
+  ProofContext.print_thms_containing (ProofContext.init (the_context ())) None ss;
 
 val welcome = priority o Session.welcome;
 val help = welcome;