src/Pure/PIDE/query_operation.ML
author wenzelm
Sun Mar 10 14:19:30 2019 +0100 (4 months ago ago)
changeset 70070 be04e9a053a7
parent 62923 3a122e1e352a
permissions -rw-r--r--
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
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@60610
    10
  val register: {name: string, pri: int} ->
wenzelm@61223
    11
    ({state: Toplevel.state, args: string list,
wenzelm@61223
    12
      output_result: string -> unit, writeln_result: string -> unit} -> unit) -> unit
wenzelm@52865
    13
end;
wenzelm@52865
    14
wenzelm@52865
    15
structure Query_Operation: QUERY_OPERATION =
wenzelm@52865
    16
struct
wenzelm@52865
    17
wenzelm@60610
    18
fun register {name, pri} f =
wenzelm@61206
    19
  Command.print_function (name ^ "_query")
wenzelm@52865
    20
    (fn {args = instance :: args, ...} =>
wenzelm@61208
    21
      SOME {delay = NONE, pri = pri, persistent = false, strict = false,
wenzelm@62923
    22
        print_fn = fn _ => Thread_Attributes.uninterruptible (fn restore_attributes => fn state =>
wenzelm@61208
    23
          let
wenzelm@61223
    24
            fun output_result s = Output.result [(Markup.instanceN, instance)] [s];
wenzelm@61223
    25
            fun status m = output_result (Markup.markup_only m);
wenzelm@61223
    26
            fun writeln_result s = output_result (Markup.markup Markup.writeln s);
wenzelm@61223
    27
            fun toplevel_error exn =
wenzelm@61223
    28
              output_result (Markup.markup Markup.error (Runtime.exn_message exn));
wenzelm@52876
    29
wenzelm@61208
    30
            val _ = status Markup.running;
wenzelm@61223
    31
            fun run () =
wenzelm@61223
    32
              f {state = state, args = args, output_result = output_result,
wenzelm@61223
    33
                  writeln_result = writeln_result};
wenzelm@61208
    34
            val _ =
wenzelm@61208
    35
              (case Exn.capture (*sic!*) (restore_attributes run) () of
wenzelm@61208
    36
                Exn.Res () => ()
wenzelm@61208
    37
              | Exn.Exn exn => toplevel_error exn);
wenzelm@61208
    38
            val _ = status Markup.finished;
wenzelm@61208
    39
          in () end)}
wenzelm@61208
    40
    | _ => NONE);
wenzelm@61208
    41
wenzelm@61208
    42
wenzelm@61208
    43
(* print_state *)
wenzelm@61208
    44
wenzelm@61208
    45
val _ =
wenzelm@61214
    46
  register {name = "print_state", pri = Task_Queue.urgent_pri}
wenzelm@61208
    47
    (fn {state = st, output_result, ...} =>
wenzelm@61208
    48
      if Toplevel.is_proof st
wenzelm@61209
    49
      then output_result (Markup.markup Markup.state (Toplevel.string_of_state st))
wenzelm@61208
    50
      else ());
wenzelm@52865
    51
wenzelm@52865
    52
end;