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};
     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 -> Pretty.T list) -> 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"
    22     ([]: (string * (string * (Toplevel.state -> Pretty.T list))) list);
    23 
    24 fun 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 
    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 =>
    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 
    47 val _ =
    48   Query_Operation.register "print_operation" (fn {state, args, output_result} =>
    49     let
    50       val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
    51       fun err s = Pretty.mark_str (Markup.bad, s);
    52       fun print name =
    53         (case AList.lookup (op =) (Synchronized.value print_operations) name of
    54           SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"])
    55         | NONE => [err ("Unknown print operation: " ^ quote name)]);
    56     in output_result (Pretty.string_of (Pretty.chunks (maps print args))) end);
    57 
    58 end;
    59 
    60 
    61 (* common print operations *)
    62 
    63 val _ =
    64   register "context" "context of local theory target" Toplevel.pretty_context;
    65 
    66 val _ =
    67   register "cases" "cases of proof context"
    68     (Proof_Context.pretty_cases o Toplevel.context_of);
    69 
    70 val _ =
    71   register "terms" "term bindings of proof context"
    72     (Proof_Context.pretty_term_bindings o Toplevel.context_of);
    73 
    74 val _ =
    75   register "theorems" "theorems of local theory or proof context"
    76     (Isar_Cmd.pretty_theorems false);
    77 
    78 val _ =
    79   register "state" "proof state" Toplevel.pretty_state;
    80 
    81 end;
    82