src/Pure/PIDE/query_operation.ML
author wenzelm
Tue Aug 12 18:36:43 2014 +0200 (2014-08-12)
changeset 57916 2c2c24dbf0a4
parent 57872 28e17057b545
child 60610 f52b4b0c10c4
permissions -rw-r--r--
generic process wrapping in Prover;
clarified module arrangement;
wenzelm@52865
     1
(*  Title:      Pure/PIDE/query_operation.ML
wenzelm@52865
     2
    Author:     Makarius
wenzelm@52865
     3
wenzelm@52865
     4
One-shot query operations via asynchronous print functions and temporary
wenzelm@57872
     5
document overlays.
wenzelm@52865
     6
*)
wenzelm@52865
     7
wenzelm@52865
     8
signature QUERY_OPERATION =
wenzelm@52865
     9
sig
wenzelm@52982
    10
  val register: string ->
wenzelm@52982
    11
    ({state: Toplevel.state, args: string list, output_result: string -> unit} -> unit) -> unit
wenzelm@52865
    12
end;
wenzelm@52865
    13
wenzelm@52865
    14
structure Query_Operation: QUERY_OPERATION =
wenzelm@52865
    15
struct
wenzelm@52865
    16
wenzelm@52982
    17
fun register name f =
wenzelm@52865
    18
  Command.print_function name
wenzelm@52865
    19
    (fn {args = instance :: args, ...} =>
wenzelm@52953
    20
        SOME {delay = NONE, pri = 0, persistent = false, strict = false,
wenzelm@52931
    21
          print_fn = fn _ => uninterruptible (fn restore_attributes => fn state =>
wenzelm@52865
    22
            let
wenzelm@56333
    23
              fun result s = Output.result [(Markup.instanceN, instance)] [s];
wenzelm@52876
    24
              fun status m = result (Markup.markup_only m);
wenzelm@52982
    25
              fun output_result s = result (Markup.markup (Markup.writelnN, []) s);
wenzelm@52929
    26
              fun toplevel_error exn =
wenzelm@56303
    27
                result (Markup.markup (Markup.errorN, []) (Runtime.exn_message exn));
wenzelm@52876
    28
wenzelm@52876
    29
              val _ = status Markup.running;
wenzelm@52982
    30
              fun run () = f {state = state, args = args, output_result = output_result};
wenzelm@52982
    31
              val _ =
wenzelm@52982
    32
                (case Exn.capture (*sic!*) (restore_attributes run) () of
wenzelm@52982
    33
                  Exn.Res () => ()
wenzelm@52982
    34
                | Exn.Exn exn => toplevel_error exn);
wenzelm@52876
    35
              val _ = status Markup.finished;
wenzelm@52931
    36
            in () end)}
wenzelm@52865
    37
      | _ => NONE);
wenzelm@52865
    38
wenzelm@52865
    39
end;
wenzelm@52865
    40