src/Pure/Tools/find_theorems.ML
changeset 52942 07093b66fc9d
parent 52941 28407b5f1c72
child 52943 14ddcc0ad7df
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Aug 09 15:49:50 2013 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Aug 09 16:17:48 2013 +0200
     1.3 @@ -576,10 +576,13 @@
     1.4  (** PIDE query operation **)
     1.5  
     1.6  val _ =
     1.7 -  Query_Operation.register "find_theorems" (fn st => fn args =>
     1.8 +  Query_Operation.register "find_theorems" (fn st => fn [limit_arg, allow_dups_arg, query_arg] =>
     1.9      if can Toplevel.context_of st then
    1.10 -      Pretty.string_of
    1.11 -        (pretty_theorems (proof_state st) NONE false (maps (read_query Position.none) args))
    1.12 +      let
    1.13 +        val opt_limit = Int.fromString limit_arg;
    1.14 +        val rem_dups = allow_dups_arg = "false";
    1.15 +        val criteria = read_query Position.none query_arg;
    1.16 +      in Pretty.string_of (pretty_theorems (proof_state st) opt_limit rem_dups criteria) end
    1.17      else error "Unknown context");
    1.18  
    1.19  end;