src/Pure/Tools/find_theorems.ML
changeset 52982 8e78bd316a53
parent 52955 797362ce0c14
child 53632 96808429b9ec
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Aug 12 17:17:49 2013 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Aug 12 17:57:51 2013 +0200
     1.3 @@ -575,17 +575,17 @@
     1.4  (** PIDE query operation **)
     1.5  
     1.6  val _ =
     1.7 -  Query_Operation.register "find_theorems"
     1.8 -    (fn st => fn [limit_arg, allow_dups_arg, context_arg, query_arg] =>
     1.9 -      if can Toplevel.context_of st then
    1.10 -        let
    1.11 -          val state =
    1.12 -            if context_arg = "" then proof_state st
    1.13 -            else Proof.init (Proof_Context.init_global (Thy_Info.get_theory context_arg));
    1.14 -          val opt_limit = Int.fromString limit_arg;
    1.15 -          val rem_dups = allow_dups_arg = "false";
    1.16 -          val criteria = read_query Position.none query_arg;
    1.17 -        in Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria) end
    1.18 -      else error "Unknown context");
    1.19 +  Query_Operation.register "find_theorems" (fn {state = st, args, output_result} =>
    1.20 +    if can Toplevel.context_of st then
    1.21 +      let
    1.22 +        val [limit_arg, allow_dups_arg, context_arg, query_arg] = args;
    1.23 +        val state =
    1.24 +          if context_arg = "" then proof_state st
    1.25 +          else Proof.init (Proof_Context.init_global (Thy_Info.get_theory context_arg));
    1.26 +        val opt_limit = Int.fromString limit_arg;
    1.27 +        val rem_dups = allow_dups_arg = "false";
    1.28 +        val criteria = read_query Position.none query_arg;
    1.29 +      in output_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end
    1.30 +    else error "Unknown context");
    1.31  
    1.32  end;