src/Pure/PIDE/query_operation.ML
author wenzelm
Sat Mar 01 22:46:31 2014 +0100 (2014-03-01)
changeset 55828 42ac3cfb89f6
parent 52982 8e78bd316a53
child 56303 4cc3f4db3447
permissions -rw-r--r--
clarified language markup: added "delimited" property;
type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche);
observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
     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