src/Pure/Tools/find_theorems.ML
changeset 52943 14ddcc0ad7df
parent 52942 07093b66fc9d
child 52954 b8b77a148ada
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Aug 09 16:17:48 2013 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Aug 09 17:25:47 2013 +0200
     1.3 @@ -576,13 +576,17 @@
     1.4  (** PIDE query operation **)
     1.5  
     1.6  val _ =
     1.7 -  Query_Operation.register "find_theorems" (fn st => fn [limit_arg, allow_dups_arg, query_arg] =>
     1.8 -    if can Toplevel.context_of st then
     1.9 -      let
    1.10 -        val opt_limit = Int.fromString limit_arg;
    1.11 -        val rem_dups = allow_dups_arg = "false";
    1.12 -        val criteria = read_query Position.none query_arg;
    1.13 -      in Pretty.string_of (pretty_theorems (proof_state st) opt_limit rem_dups criteria) end
    1.14 -    else error "Unknown context");
    1.15 +  Query_Operation.register "find_theorems"
    1.16 +    (fn st => fn [limit_arg, allow_dups_arg, context_arg, query_arg] =>
    1.17 +      if can Toplevel.context_of st then
    1.18 +        let
    1.19 +          val state =
    1.20 +            if context_arg = "" then proof_state st
    1.21 +            else Proof.init (Proof_Context.init_global (Thy_Info.get_theory context_arg));
    1.22 +          val opt_limit = Int.fromString limit_arg;
    1.23 +          val rem_dups = allow_dups_arg = "false";
    1.24 +          val criteria = read_query Position.none query_arg;
    1.25 +        in Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria) end
    1.26 +      else error "Unknown context");
    1.27  
    1.28  end;