56864
|
1 |
(* Title: Pure/Tools/print_operation.ML
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Print operations as asynchronous query.
|
|
5 |
*)
|
|
6 |
|
|
7 |
|
|
8 |
signature PRINT_OPERATION =
|
|
9 |
sig
|
|
10 |
val register: string -> string -> (Toplevel.state -> string) -> unit
|
|
11 |
end;
|
|
12 |
|
|
13 |
structure Print_Operation: PRINT_OPERATION =
|
|
14 |
struct
|
|
15 |
|
|
16 |
(* maintain print operations *)
|
|
17 |
|
|
18 |
local
|
|
19 |
|
|
20 |
val print_operations =
|
|
21 |
Synchronized.var "print_operations"
|
56867
|
22 |
([]: (string * (string * (Toplevel.state -> string))) list);
|
56864
|
23 |
|
|
24 |
fun report () =
|
|
25 |
Output.try_protocol_message Markup.print_operations
|
|
26 |
let
|
|
27 |
val yxml =
|
56867
|
28 |
Synchronized.value print_operations
|
|
29 |
|> map (fn (x, (y, _)) => (x, y)) |> rev
|
56864
|
30 |
|> let open XML.Encode in list (pair string string) end
|
|
31 |
|> YXML.string_of_body;
|
|
32 |
in [yxml] end;
|
|
33 |
|
|
34 |
val _ = Isabelle_Process.protocol_command "print_operations" (fn [] => report ());
|
|
35 |
|
|
36 |
val _ = Session.protocol_handler "isabelle.Print_Operation$Handler";
|
|
37 |
|
|
38 |
in
|
|
39 |
|
|
40 |
fun register name description pr =
|
|
41 |
(Synchronized.change print_operations (fn tab =>
|
56867
|
42 |
(if not (AList.defined (op =) tab name) then ()
|
56864
|
43 |
else warning ("Redefining print operation: " ^ quote name);
|
56867
|
44 |
AList.update (op =) (name, (description, pr)) tab));
|
56864
|
45 |
report ());
|
|
46 |
|
|
47 |
val _ =
|
|
48 |
Query_Operation.register "print_operation" (fn {state, args, output_result} =>
|
|
49 |
let
|
|
50 |
val [name] = args;
|
|
51 |
val pr =
|
56867
|
52 |
(case AList.lookup (op =) (Synchronized.value print_operations) name of
|
56864
|
53 |
SOME (_, pr) => pr
|
|
54 |
| NONE => error ("Unknown print operation: " ^ quote name));
|
|
55 |
val result = pr state handle Toplevel.UNDEF => error "Unknown context";
|
|
56 |
in output_result result end);
|
|
57 |
|
|
58 |
end;
|
|
59 |
|
|
60 |
|
|
61 |
(* common print operations *)
|
|
62 |
|
|
63 |
val _ =
|
56867
|
64 |
register "context" "main context"
|
|
65 |
(Pretty.string_of o Pretty.chunks o Toplevel.pretty_state_context);
|
|
66 |
|
|
67 |
val _ =
|
|
68 |
register "cases" "cases of proof context"
|
|
69 |
(Pretty.string_of o Pretty.chunks o Proof_Context.pretty_cases o Toplevel.context_of);
|
|
70 |
|
|
71 |
val _ =
|
|
72 |
register "binds" "term bindings of proof context"
|
|
73 |
(Pretty.string_of o Pretty.chunks o Proof_Context.pretty_binds o Toplevel.context_of);
|
|
74 |
|
|
75 |
val _ =
|
|
76 |
register "facts" "facts of proof context"
|
56864
|
77 |
(fn st =>
|
|
78 |
Proof_Context.pretty_local_facts (Toplevel.context_of st) false
|
|
79 |
|> Pretty.chunks |> Pretty.string_of);
|
|
80 |
|
56867
|
81 |
val _ =
|
|
82 |
register "state" "proof state"
|
|
83 |
(Pretty.string_of o Pretty.chunks o Toplevel.pretty_state true);
|
|
84 |
|
56864
|
85 |
end;
|
|
86 |
|