src/Pure/Tools/find_consts.ML
changeset 60610 f52b4b0c10c4
parent 59936 b8ffc3dc9e24
child 60664 263a8f15faf3
     1.1 --- a/src/Pure/Tools/find_consts.ML	Mon Jun 29 19:27:07 2015 +0200
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Mon Jun 29 20:55:46 2015 +0200
     1.3 @@ -163,14 +163,15 @@
     1.4  (* PIDE query operation *)
     1.5  
     1.6  val _ =
     1.7 -  Query_Operation.register "find_consts" (fn {state, args, output_result} =>
     1.8 -    (case try Toplevel.context_of state of
     1.9 -      SOME ctxt =>
    1.10 -        let
    1.11 -          val [query_arg] = args;
    1.12 -          val query = read_query Position.none query_arg;
    1.13 -        in output_result (Pretty.string_of (pretty_consts ctxt query)) end
    1.14 -    | NONE => error "Unknown context"));
    1.15 +  Query_Operation.register {name = "find_consts", pri = Task_Queue.urgent_pri}
    1.16 +    (fn {state, args, output_result} =>
    1.17 +      (case try Toplevel.context_of state of
    1.18 +        SOME ctxt =>
    1.19 +          let
    1.20 +            val [query_arg] = args;
    1.21 +            val query = read_query Position.none query_arg;
    1.22 +          in output_result (Pretty.string_of (pretty_consts ctxt query)) end
    1.23 +      | NONE => error "Unknown context"));
    1.24  
    1.25  end;
    1.26