src/Pure/Isar/isar_syn.ML
changeset 15964 f2074e12d1d4
parent 15801 d2f5ca3c048d
child 15979 c81578ac2d31
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Mon May 16 09:34:20 2005 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon May 16 09:35:05 2005 +0200
     1.3 @@ -631,10 +631,30 @@
     1.4      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
     1.5  
     1.6  val thms_containingP =
     1.7 -  OuterSyntax.improper_command "thms_containing"
     1.8 -    "print facts containing certain constants or variables"
     1.9 -    K.diag (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
    1.10 -      Scan.repeat P.term >> (Toplevel.no_timing oo IsarCmd.print_thms_containing));
    1.11 +  let
    1.12 +    (* intro, elim, dest and rewrite are reserved, otherwise it's a pattern *)
    1.13 +    fun decode "intro" = ProofContext.Intro
    1.14 +      | decode "elim" = ProofContext.Elim
    1.15 +      | decode "dest" = ProofContext.Dest
    1.16 +      | decode "rewrite" = ProofContext.Rewrite
    1.17 +      | decode x = ProofContext.Pattern x;
    1.18 +  
    1.19 +    (* either name:term or term *)
    1.20 +    val criterion = ((P.term :-- (fn "name" => P.$$$ ":" |-- P.term | 
    1.21 +                                     _ => Scan.fail)
    1.22 +                                 ) >> (ProofContext.Name o #2)) ||
    1.23 +                    (P.term >> decode);
    1.24 +  in
    1.25 +    OuterSyntax.improper_command "thms_containing"
    1.26 +      "print facts meeting specified criteria"
    1.27 +      K.diag 
    1.28 +      (* obtain (int option * (bool * string) list) representing
    1.29 +         a limit and a set of constraints (the bool indicates whether
    1.30 +         the constraint is inclusive or exclusive) *)
    1.31 +      (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
    1.32 +       Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
    1.33 +        >> (Toplevel.no_timing oo IsarCmd.print_thms_containing))
    1.34 +  end;
    1.35  
    1.36  val thm_depsP =
    1.37    OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"