src/Pure/PIDE/query_operation.ML
author wenzelm
Mon Feb 17 11:14:26 2014 +0100 (2014-02-17 ago)
changeset 55526 39708e59f4b0
parent 52982 8e78bd316a53
child 56303 4cc3f4db3447
permissions -rw-r--r--
more markup;
     1 (*  Title:      Pure/PIDE/query_operation.ML
     2     Author:     Makarius
     3 
     4 One-shot query operations via asynchronous print functions and temporary
     5 document overlay.
     6 *)
     7 
     8 signature QUERY_OPERATION =
     9 sig
    10   val register: string ->
    11     ({state: Toplevel.state, args: string list, output_result: string -> unit} -> unit) -> unit
    12 end;
    13 
    14 structure Query_Operation: QUERY_OPERATION =
    15 struct
    16 
    17 fun register name f =
    18   Command.print_function name
    19     (fn {args = instance :: args, ...} =>
    20         SOME {delay = NONE, pri = 0, persistent = false, strict = false,
    21           print_fn = fn _ => uninterruptible (fn restore_attributes => fn state =>
    22             let
    23               fun result s = Output.result [(Markup.instanceN, instance)] s;
    24               fun status m = result (Markup.markup_only m);
    25               fun output_result s = result (Markup.markup (Markup.writelnN, []) s);
    26               fun toplevel_error exn =
    27                 result (Markup.markup (Markup.errorN, []) (ML_Compiler.exn_message exn));
    28 
    29               val _ = status Markup.running;
    30               fun run () = f {state = state, args = args, output_result = output_result};
    31               val _ =
    32                 (case Exn.capture (*sic!*) (restore_attributes run) () of
    33                   Exn.Res () => ()
    34                 | Exn.Exn exn => toplevel_error exn);
    35               val _ = status Markup.finished;
    36             in () end)}
    37       | _ => NONE);
    38 
    39 end;
    40