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