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