1(*  Title:      Pure/PIDE/query_operation.ML
2    Author:     Makarius
3
4One-shot query operations via asynchronous print functions and temporary
5document overlays.
6*)
7
8signature QUERY_OPERATION =
9sig
10  val register: {name: string, pri: int} ->
11    ({state: Toplevel.state, args: string list,
12      output_result: string -> unit, writeln_result: string -> unit} -> unit) -> unit
13end;
14
15structure Query_Operation: QUERY_OPERATION =
16struct
17
18fun register {name, pri} f =
19  Command.print_function (name ^ "_query")
20    (fn {args = instance :: args, ...} =>
21      SOME {delay = NONE, pri = pri, persistent = false, strict = false,
22        print_fn = fn _ => Thread_Attributes.uninterruptible (fn restore_attributes => fn state =>
23          let
24            fun output_result s = Output.result [(Markup.instanceN, instance)] [s];
25            fun status m = output_result (Markup.markup_only m);
26            fun writeln_result s = output_result (Markup.markup Markup.writeln s);
27            fun toplevel_error exn =
28              output_result (Markup.markup Markup.error (Runtime.exn_message exn));
29
30            val _ = status Markup.running;
31            fun run () =
32              f {state = state, args = args, output_result = output_result,
33                  writeln_result = writeln_result};
34            val _ =
35              (case Exn.capture (*sic!*) (restore_attributes run) () of
36                Exn.Res () => ()
37              | Exn.Exn exn => toplevel_error exn);
38            val _ = status Markup.finished;
39          in () end)}
40    | _ => NONE);
41
42
43(* print_state *)
44
45val _ =
46  register {name = "print_state", pri = Task_Queue.urgent_pri}
47    (fn {state = st, output_result, ...} =>
48      if Toplevel.is_proof st
49      then output_result (Markup.markup Markup.state (Toplevel.string_of_state st))
50      else ());
51
52end;
53