# HG changeset patch # User wenzelm # Date 1281541829 -7200 # Node ID c677c2c1d333addf6d76a394ca5bed304eb78bd9 # Parent 3f4fadad94973451cd74bf5e2a3035d82d7b5335 simplified/unified command setup; diff -r 3f4fadad9497 -r c677c2c1d333 src/Pure/Tools/find_consts.ML --- a/src/Pure/Tools/find_consts.ML Wed Aug 11 17:37:04 2010 +0200 +++ b/src/Pure/Tools/find_consts.ML Wed Aug 11 17:50:29 2010 +0200 @@ -144,19 +144,22 @@ (* command syntax *) -fun find_consts_cmd spec = - Toplevel.unknown_theory o Toplevel.keep (fn state => - find_consts (Proof.context_of (Toplevel.enter_proof_body state)) spec); +local val criterion = Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Strict || Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name || Parse.xname >> Loose; +in + val _ = Outer_Syntax.improper_command "find_consts" "search constants by type pattern" Keyword.diag (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion) - >> (Toplevel.no_timing oo find_consts_cmd)); + >> (fn spec => Toplevel.no_timing o + Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec))); end; +end; + diff -r 3f4fadad9497 -r c677c2c1d333 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Wed Aug 11 17:37:04 2010 +0200 +++ b/src/Pure/Tools/find_theorems.ML Wed Aug 11 17:50:29 2010 +0200 @@ -455,14 +455,6 @@ (** command syntax **) -fun find_theorems_cmd ((opt_lim, rem_dups), spec) = - Toplevel.unknown_theory o Toplevel.keep (fn state => - let - val proof_state = Toplevel.enter_proof_body state; - val ctxt = Proof.context_of proof_state; - val opt_goal = try Proof.simple_goal proof_state |> Option.map #goal; - in print_theorems ctxt opt_goal opt_lim rem_dups spec end); - local val criterion = @@ -486,7 +478,13 @@ Outer_Syntax.improper_command "find_theorems" "print theorems meeting specified criteria" Keyword.diag (options -- Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion)) - >> (Toplevel.no_timing oo find_theorems_cmd)); + >> (fn ((opt_lim, rem_dups), spec) => + Toplevel.no_timing o + Toplevel.keep (fn state => + let + val ctxt = Toplevel.context_of state; + val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal; + in print_theorems ctxt opt_goal opt_lim rem_dups spec end))); end;