src/Pure/Tools/print_operation.ML
changeset 56864 0446c7ac2e32
child 56867 224109105008
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/print_operation.ML	Mon May 05 15:17:07 2014 +0200
@@ -0,0 +1,70 @@
+(*  Title:      Pure/Tools/print_operation.ML
+    Author:     Makarius
+
+Print operations as asynchronous query.
+*)
+
+
+signature PRINT_OPERATION =
+sig
+  val register: string -> string -> (Toplevel.state -> string) -> unit
+end;
+
+structure Print_Operation: PRINT_OPERATION =
+struct
+
+(* maintain print operations *)
+
+local
+
+val print_operations =
+  Synchronized.var "print_operations"
+    (Symtab.empty: (string * (Toplevel.state -> string)) Symtab.table);
+
+fun report () =
+  Output.try_protocol_message Markup.print_operations
+    let
+      val yxml =
+        Symtab.fold (fn (x, (y, _)) => cons (x, y)) (Synchronized.value print_operations) []
+        |> sort_wrt #1
+        |> let open XML.Encode in list (pair string string) end
+        |> YXML.string_of_body;
+    in [yxml] end;
+
+val _ = Isabelle_Process.protocol_command "print_operations" (fn [] => report ());
+
+val _ = Session.protocol_handler "isabelle.Print_Operation$Handler";
+
+in
+
+fun register name description pr =
+ (Synchronized.change print_operations (fn tab =>
+   (if not (Symtab.defined tab name) then ()
+    else warning ("Redefining print operation: " ^ quote name);
+    Symtab.update (name, (description, pr)) tab));
+  report ());
+
+val _ =
+  Query_Operation.register "print_operation" (fn {state, args, output_result} =>
+    let
+      val [name] = args;
+      val pr =
+        (case Symtab.lookup (Synchronized.value print_operations) name of
+          SOME (_, pr) => pr
+        | NONE => error ("Unknown print operation: " ^ quote name));
+      val result = pr state handle Toplevel.UNDEF => error "Unknown context";
+    in output_result result end);
+
+end;
+
+
+(* common print operations *)
+
+val _ =
+  register "facts" "print facts of proof context"
+    (fn st =>
+      Proof_Context.pretty_local_facts (Toplevel.context_of st) false
+      |> Pretty.chunks |> Pretty.string_of);
+
+end;
+