src/Pure/PIDE/query_operation.ML
author wenzelm
Sat May 03 22:47:43 2014 +0200 (2014-05-03 ago)
changeset 56843 b2bfcd8cda80
parent 56333 38f1422ef473
child 57872 28e17057b545
permissions -rw-r--r--
support for path completion based on file-system content;
     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, []) (Runtime.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