1(* Title: Pure/PIDE/query_operation.ML 2 Author: Makarius 3 4One-shot query operations via asynchronous print functions and temporary 5document overlays. 6*) 7 8signature QUERY_OPERATION = 9sig 10 val register: {name: string, pri: int} -> 11 ({state: Toplevel.state, args: string list, 12 output_result: string -> unit, writeln_result: string -> unit} -> unit) -> unit 13end; 14 15structure Query_Operation: QUERY_OPERATION = 16struct 17 18fun register {name, pri} f = 19 Command.print_function (name ^ "_query") 20 (fn {args = instance :: args, ...} => 21 SOME {delay = NONE, pri = pri, persistent = false, strict = false, 22 print_fn = fn _ => Thread_Attributes.uninterruptible (fn restore_attributes => fn state => 23 let 24 fun output_result s = Output.result [(Markup.instanceN, instance)] [s]; 25 fun status m = output_result (Markup.markup_only m); 26 fun writeln_result s = output_result (Markup.markup Markup.writeln s); 27 fun toplevel_error exn = 28 output_result (Markup.markup Markup.error (Runtime.exn_message exn)); 29 30 val _ = status Markup.running; 31 fun run () = 32 f {state = state, args = args, output_result = output_result, 33 writeln_result = writeln_result}; 34 val _ = 35 (case Exn.capture (*sic!*) (restore_attributes run) () of 36 Exn.Res () => () 37 | Exn.Exn exn => toplevel_error exn); 38 val _ = status Markup.finished; 39 in () end)} 40 | _ => NONE); 41 42 43(* print_state *) 44 45val _ = 46 register {name = "print_state", pri = Task_Queue.urgent_pri} 47 (fn {state = st, output_result, ...} => 48 if Toplevel.is_proof st 49 then output_result (Markup.markup Markup.state (Toplevel.string_of_state st)) 50 else ()); 51 52end; 53