simplified/unified command setup;
authorwenzelm
Wed Aug 11 17:50:29 2010 +0200 (2010-08-11)
changeset 38334c677c2c1d333
parent 38333 3f4fadad9497
child 38335 630f379f2660
simplified/unified command setup;
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Tools/find_consts.ML	Wed Aug 11 17:37:04 2010 +0200
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Wed Aug 11 17:50:29 2010 +0200
     1.3 @@ -144,19 +144,22 @@
     1.4  
     1.5  (* command syntax *)
     1.6  
     1.7 -fun find_consts_cmd spec =
     1.8 -  Toplevel.unknown_theory o Toplevel.keep (fn state =>
     1.9 -    find_consts (Proof.context_of (Toplevel.enter_proof_body state)) spec);
    1.10 +local
    1.11  
    1.12  val criterion =
    1.13    Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Strict ||
    1.14    Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
    1.15    Parse.xname >> Loose;
    1.16  
    1.17 +in
    1.18 +
    1.19  val _ =
    1.20    Outer_Syntax.improper_command "find_consts" "search constants by type pattern" Keyword.diag
    1.21      (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
    1.22 -      >> (Toplevel.no_timing oo find_consts_cmd));
    1.23 +      >> (fn spec => Toplevel.no_timing o
    1.24 +        Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
    1.25  
    1.26  end;
    1.27  
    1.28 +end;
    1.29 +
     2.1 --- a/src/Pure/Tools/find_theorems.ML	Wed Aug 11 17:37:04 2010 +0200
     2.2 +++ b/src/Pure/Tools/find_theorems.ML	Wed Aug 11 17:50:29 2010 +0200
     2.3 @@ -455,14 +455,6 @@
     2.4  
     2.5  (** command syntax **)
     2.6  
     2.7 -fun find_theorems_cmd ((opt_lim, rem_dups), spec) =
     2.8 -  Toplevel.unknown_theory o Toplevel.keep (fn state =>
     2.9 -    let
    2.10 -      val proof_state = Toplevel.enter_proof_body state;
    2.11 -      val ctxt = Proof.context_of proof_state;
    2.12 -      val opt_goal = try Proof.simple_goal proof_state |> Option.map #goal;
    2.13 -    in print_theorems ctxt opt_goal opt_lim rem_dups spec end);
    2.14 -
    2.15  local
    2.16  
    2.17  val criterion =
    2.18 @@ -486,7 +478,13 @@
    2.19    Outer_Syntax.improper_command "find_theorems" "print theorems meeting specified criteria"
    2.20      Keyword.diag
    2.21      (options -- Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion))
    2.22 -      >> (Toplevel.no_timing oo find_theorems_cmd));
    2.23 +      >> (fn ((opt_lim, rem_dups), spec) =>
    2.24 +        Toplevel.no_timing o
    2.25 +        Toplevel.keep (fn state =>
    2.26 +          let
    2.27 +            val ctxt = Toplevel.context_of state;
    2.28 +            val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
    2.29 +          in print_theorems ctxt opt_goal opt_lim rem_dups spec end)));
    2.30  
    2.31  end;
    2.32