src/Pure/Tools/find_theorems.ML
changeset 52865 02a7e7180ee5
parent 52863 acbced24e5fc
child 52925 71e938856a03
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Aug 05 16:12:03 2013 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Aug 05 17:14:02 2013 +0200
     1.3 @@ -605,7 +605,7 @@
     1.4  
     1.5  
     1.6  
     1.7 -(** command syntax **)
     1.8 +(** Isar command syntax **)
     1.9  
    1.10  local
    1.11  
    1.12 @@ -647,28 +647,10 @@
    1.13  
    1.14  
    1.15  
    1.16 -(** print function **)
    1.17 -
    1.18 -val find_theoremsN = "find_theorems";
    1.19 +(** PIDE query operation **)
    1.20  
    1.21 -val _ = Command.print_function find_theoremsN
    1.22 -  (fn {args, ...} =>
    1.23 -    (case args of
    1.24 -      [instance, query] =>
    1.25 -      SOME {delay = NONE, pri = 0, persistent = false,
    1.26 -        print_fn = fn _ => fn state =>
    1.27 -          let
    1.28 -            val msg =
    1.29 -              XML.Elem ((Markup.writelnN, []),
    1.30 -                [XML.Text
    1.31 -                  (Pretty.string_of (pretty_theorems_cmd state NONE false (parse_query query)))])
    1.32 -              handle exn =>
    1.33 -                if Exn.is_interrupt exn then reraise exn
    1.34 -                else XML.Elem ((Markup.errorN, []), [XML.Text (ML_Compiler.exn_message exn)]);
    1.35 -          in
    1.36 -            Output.result [(Markup.kindN, find_theoremsN), (Markup.instanceN, instance)]
    1.37 -              (YXML.string_of msg)
    1.38 -          end}
    1.39 -    | _ => NONE));
    1.40 +val _ =
    1.41 +  Query_Operation.register "find_theorems" (fn state => fn query =>
    1.42 +    Pretty.string_of (pretty_theorems_cmd state NONE false (maps parse_query query)));
    1.43  
    1.44  end;