--- a/src/Pure/Tools/find_theorems.ML Mon Aug 12 17:17:49 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML Mon Aug 12 17:57:51 2013 +0200
@@ -575,17 +575,17 @@
(** PIDE query operation **)
val _ =
- 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");
+ Query_Operation.register "find_theorems" (fn {state = st, args, output_result} =>
+ if can Toplevel.context_of st then
+ let
+ val [limit_arg, allow_dups_arg, context_arg, query_arg] = args;
+ 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 output_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end
+ else error "Unknown context");
end;