thms_containing: optional limit argument;
authorwenzelm
Tue Jul 02 17:44:13 2002 +0200 (2002-07-02)
changeset 1328420c818c966e6
parent 13283 1051aa66cbf3
child 13285 28d1823ce0f2
thms_containing: optional limit argument;
NEWS
doc-src/IsarRef/pure.tex
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/proof_context.ML
src/Pure/proof_general.ML
     1.1 --- a/NEWS	Tue Jul 02 17:00:05 2002 +0200
     1.2 +++ b/NEWS	Tue Jul 02 17:44:13 2002 +0200
     1.3 @@ -9,7 +9,9 @@
     1.4  
     1.5  * improved thms_containing: proper indexing of facts instead of raw
     1.6  theorems; check validity of results wrt. current name space; include
     1.7 -local facts of proof configuration (also covers active locales);
     1.8 +local facts of proof configuration (also covers active locales); an
     1.9 +optional limit for the number of printed facts may be given (the
    1.10 +default is 40);
    1.11  
    1.12  
    1.13  *** HOL ***
     2.1 --- a/doc-src/IsarRef/pure.tex	Tue Jul 02 17:00:05 2002 +0200
     2.2 +++ b/doc-src/IsarRef/pure.tex	Tue Jul 02 17:44:13 2002 +0200
     2.3 @@ -1355,7 +1355,7 @@
     2.4  \railterm{thmdeps}
     2.5  
     2.6  \begin{rail}
     2.7 -  thmscontaining (term * )
     2.8 +  thmscontaining ('(' nat ')')? (term * )
     2.9    ;
    2.10    thmdeps thmrefs
    2.11    ;
    2.12 @@ -1391,7 +1391,8 @@
    2.13  \item [$\isarkeyword{thms_containing}~\vec t$] retrieves facts from the theory
    2.14    or proof context containing all of the constants or variables occurring in
    2.15    terms $\vec t$.  Note that giving the empty list yields \emph{all} currently
    2.16 -  known facts.
    2.17 +  known facts.  An optional limit for the number printed facts may be given;
    2.18 +  the default is 40.
    2.19    
    2.20  \item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of facts,
    2.21    using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
     3.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Jul 02 17:00:05 2002 +0200
     3.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Jul 02 17:44:13 2002 +0200
     3.3 @@ -54,7 +54,8 @@
     3.4    val print_trans_rules: Toplevel.transition -> Toplevel.transition
     3.5    val print_methods: Toplevel.transition -> Toplevel.transition
     3.6    val print_antiquotations: Toplevel.transition -> Toplevel.transition
     3.7 -  val print_thms_containing: string list -> Toplevel.transition -> Toplevel.transition
     3.8 +  val print_thms_containing: int option * string list
     3.9 +    -> Toplevel.transition -> Toplevel.transition
    3.10    val thm_deps: (string * Args.src list) list -> Toplevel.transition -> Toplevel.transition
    3.11    val print_binds: Toplevel.transition -> Toplevel.transition
    3.12    val print_lthms: Toplevel.transition -> Toplevel.transition
    3.13 @@ -224,9 +225,9 @@
    3.14  
    3.15  val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations;
    3.16  
    3.17 -fun print_thms_containing ss = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    3.18 +fun print_thms_containing (lim, spec) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    3.19    ProofContext.print_thms_containing
    3.20 -    (Toplevel.node_case ProofContext.init Proof.context_of state) ss);
    3.21 +    (Toplevel.node_case ProofContext.init Proof.context_of state) lim spec);
    3.22  
    3.23  fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    3.24    ThmDeps.thm_deps (IsarThy.get_thmss args (Toplevel.enter_forward_proof state)));
     4.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Jul 02 17:00:05 2002 +0200
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Jul 02 17:44:13 2002 +0200
     4.3 @@ -583,7 +583,8 @@
     4.4  val thms_containingP =
     4.5    OuterSyntax.improper_command "thms_containing"
     4.6      "print facts containing certain constants or variables"
     4.7 -    K.diag (Scan.repeat P.term >> (Toplevel.no_timing oo IsarCmd.print_thms_containing));
     4.8 +    K.diag (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
     4.9 +      Scan.repeat P.term >> (Toplevel.no_timing oo IsarCmd.print_thms_containing));
    4.10  
    4.11  val thm_depsP =
    4.12    OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
     5.1 --- a/src/Pure/Isar/proof_context.ML	Tue Jul 02 17:00:05 2002 +0200
     5.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Jul 02 17:44:13 2002 +0200
     5.3 @@ -125,7 +125,8 @@
     5.4    val prems_limit: int ref
     5.5    val pretty_asms: context -> Pretty.T list
     5.6    val pretty_context: context -> Pretty.T list
     5.7 -  val print_thms_containing: context -> string list -> unit
     5.8 +  val thms_containing_limit: int ref
     5.9 +  val print_thms_containing: context -> int option -> string list -> unit
    5.10    val setup: (theory -> theory) list
    5.11  end;
    5.12  
    5.13 @@ -1378,7 +1379,9 @@
    5.14    in gen_distinct eq_fst (filter valid (FactIndex.find idx index)) end;
    5.15  
    5.16  
    5.17 -fun print_thms_containing ctxt ss =
    5.18 +val thms_containing_limit = ref 40;
    5.19 +
    5.20 +fun print_thms_containing ctxt opt_limit ss =
    5.21    let
    5.22      val prt_term = pretty_term ctxt;
    5.23      val prt_fact = pretty_fact ctxt;
    5.24 @@ -1398,13 +1401,16 @@
    5.25        else [Pretty.block (Pretty.breaks (Pretty.str "Facts containing" ::
    5.26          separate (Pretty.str "and") (prt_consts cs @ prt_frees xs)) @
    5.27            [Pretty.str ":", Pretty.fbrk])]
    5.28 -    val globals = PureThy.thms_containing (theory_of ctxt) (cs, xs);
    5.29 -    val locals = lthms_containing ctxt (cs, xs);
    5.30 +    val facts =
    5.31 +      PureThy.thms_containing (theory_of ctxt) (cs, xs) @ lthms_containing ctxt (cs, xs)
    5.32 +      |> sort_wrt #1;
    5.33 +    val len = length facts;
    5.34 +    val limit = if_none opt_limit (! thms_containing_limit);
    5.35    in
    5.36      if empty_idx andalso not (Library.null ss) then
    5.37        warning "thms_containing: no consts/frees in specification"
    5.38 -    else (header @ map prt_fact (sort_wrt #1 (globals @ locals)))
    5.39 -      |> Pretty.chunks |> Pretty.writeln
    5.40 +    else (header @ (if len <= limit then [] else [Pretty.str "..."]) @
    5.41 +        map prt_fact (Library.drop (len - limit, facts))) |> Pretty.chunks |> Pretty.writeln
    5.42    end;
    5.43  
    5.44  
     6.1 --- a/src/Pure/proof_general.ML	Tue Jul 02 17:00:05 2002 +0200
     6.2 +++ b/src/Pure/proof_general.ML	Tue Jul 02 17:44:13 2002 +0200
     6.3 @@ -220,7 +220,7 @@
     6.4  (* misc commands for ProofGeneral/isa *)
     6.5  
     6.6  fun thms_containing ss =
     6.7 -  ProofContext.print_thms_containing (ProofContext.init (the_context ())) ss;
     6.8 +  ProofContext.print_thms_containing (ProofContext.init (the_context ())) None ss;
     6.9  
    6.10  val welcome = priority o Session.welcome;
    6.11  val help = welcome;