src/Pure/Tools/print_operation.ML
author wenzelm
Mon, 05 May 2014 15:17:07 +0200
changeset 56864 0446c7ac2e32
child 56867 224109105008
permissions -rw-r--r--
support print operations as asynchronous query;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56864
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Tools/print_operation.ML
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
     3
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
     4
Print operations as asynchronous query.
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
     5
*)
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
     6
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
     7
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
     8
signature PRINT_OPERATION =
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
     9
sig
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    10
  val register: string -> string -> (Toplevel.state -> string) -> unit
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    11
end;
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    12
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    13
structure Print_Operation: PRINT_OPERATION =
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    14
struct
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    15
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    16
(* maintain print operations *)
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    17
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    18
local
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    19
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    20
val print_operations =
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    21
  Synchronized.var "print_operations"
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    22
    (Symtab.empty: (string * (Toplevel.state -> string)) Symtab.table);
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    23
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    24
fun report () =
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    25
  Output.try_protocol_message Markup.print_operations
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    26
    let
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    27
      val yxml =
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    28
        Symtab.fold (fn (x, (y, _)) => cons (x, y)) (Synchronized.value print_operations) []
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    29
        |> sort_wrt #1
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    30
        |> let open XML.Encode in list (pair string string) end
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    31
        |> YXML.string_of_body;
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    32
    in [yxml] end;
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    33
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    34
val _ = Isabelle_Process.protocol_command "print_operations" (fn [] => report ());
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    35
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    36
val _ = Session.protocol_handler "isabelle.Print_Operation$Handler";
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    37
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    38
in
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    39
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    40
fun register name description pr =
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    41
 (Synchronized.change print_operations (fn tab =>
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    42
   (if not (Symtab.defined tab name) then ()
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    43
    else warning ("Redefining print operation: " ^ quote name);
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    44
    Symtab.update (name, (description, pr)) tab));
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    45
  report ());
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    46
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    47
val _ =
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    48
  Query_Operation.register "print_operation" (fn {state, args, output_result} =>
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    49
    let
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    50
      val [name] = args;
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    51
      val pr =
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    52
        (case Symtab.lookup (Synchronized.value print_operations) name of
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    53
          SOME (_, pr) => pr
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    54
        | NONE => error ("Unknown print operation: " ^ quote name));
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    55
      val result = pr state handle Toplevel.UNDEF => error "Unknown context";
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    56
    in output_result result end);
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    57
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    58
end;
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    59
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    60
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    61
(* common print operations *)
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    62
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    63
val _ =
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    64
  register "facts" "print facts of proof context"
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    65
    (fn st =>
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    66
      Proof_Context.pretty_local_facts (Toplevel.context_of st) false
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    67
      |> Pretty.chunks |> Pretty.string_of);
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    68
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    69
end;
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents:
diff changeset
    70