src/Pure/Tools/print_operation.ML
changeset 56864 0446c7ac2e32
child 56867 224109105008
equal deleted inserted replaced
56863:5fdb61a9a010 56864:0446c7ac2e32
       
     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"
       
    22     (Symtab.empty: (string * (Toplevel.state -> string)) Symtab.table);
       
    23 
       
    24 fun report () =
       
    25   Output.try_protocol_message Markup.print_operations
       
    26     let
       
    27       val yxml =
       
    28         Symtab.fold (fn (x, (y, _)) => cons (x, y)) (Synchronized.value print_operations) []
       
    29         |> sort_wrt #1
       
    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 (Symtab.defined tab name) then ()
       
    43     else warning ("Redefining print operation: " ^ quote name);
       
    44     Symtab.update (name, (description, pr)) tab));
       
    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 =
       
    52         (case Symtab.lookup (Synchronized.value print_operations) name of
       
    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 _ =
       
    64   register "facts" "print facts of proof context"
       
    65     (fn st =>
       
    66       Proof_Context.pretty_local_facts (Toplevel.context_of st) false
       
    67       |> Pretty.chunks |> Pretty.string_of);
       
    68 
       
    69 end;
       
    70