--- a/src/Pure/Tools/find_theorems.ML Fri Aug 09 16:17:48 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML Fri Aug 09 17:25:47 2013 +0200
@@ -576,13 +576,17 @@
(** PIDE query operation **)
val _ =
- Query_Operation.register "find_theorems" (fn st => fn [limit_arg, allow_dups_arg, query_arg] =>
- if can Toplevel.context_of st then
- let
- val opt_limit = Int.fromString limit_arg;
- val rem_dups = allow_dups_arg = "false";
- val criteria = read_query Position.none query_arg;
- in Pretty.string_of (pretty_theorems (proof_state st) opt_limit rem_dups criteria) end
- else error "Unknown context");
+ Query_Operation.register "find_theorems"
+ (fn st => fn [limit_arg, allow_dups_arg, context_arg, query_arg] =>
+ if can Toplevel.context_of st then
+ let
+ val state =
+ if context_arg = "" then proof_state st
+ else Proof.init (Proof_Context.init_global (Thy_Info.get_theory context_arg));
+ val opt_limit = Int.fromString limit_arg;
+ val rem_dups = allow_dups_arg = "false";
+ val criteria = read_query Position.none query_arg;
+ in Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria) end
+ else error "Unknown context");
end;