src/Pure/Tools/print_operation.ML

--- a/src/Pure/Tools/print_operation.ML	Mon May 05 16:29:09 2014 +0200
+++ b/src/Pure/Tools/print_operation.ML	Mon May 05 16:30:19 2014 +0200
@@ -19,14 +19,14 @@
 
 val print_operations =
   Synchronized.var "print_operations"
-    (Symtab.empty: (string * (Toplevel.state -> string)) Symtab.table);
+    ([]: (string * (string * (Toplevel.state -> string))) list);
 
 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
+        Synchronized.value print_operations
+        |> map (fn (x, (y, _)) => (x, y)) |> rev
         |> let open XML.Encode in list (pair string string) end
         |> YXML.string_of_body;
     in [yxml] end;
@@ -39,9 +39,9 @@
 
 fun register name description pr =
  (Synchronized.change print_operations (fn tab =>
-   (if not (Symtab.defined tab name) then ()
+   (if not (AList.defined (op =) tab name) then ()
     else warning ("Redefining print operation: " ^ quote name);
-    Symtab.update (name, (description, pr)) tab));
+    AList.update (op =) (name, (description, pr)) tab));
   report ());
 
 val _ =
@@ -49,7 +49,7 @@
     let
       val [name] = args;
       val pr =
-        (case Symtab.lookup (Synchronized.value print_operations) name of
+        (case AList.lookup (op =) (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";
@@ -61,10 +61,26 @@
 (* common print operations *)
 
 val _ =
-  register "facts" "print facts of proof context"
+  register "context" "main context"
+    (Pretty.string_of o Pretty.chunks o Toplevel.pretty_state_context);
+
+val _ =
+  register "cases" "cases of proof context"
+    (Pretty.string_of o Pretty.chunks o Proof_Context.pretty_cases o Toplevel.context_of);
+
+val _ =
+  register "binds" "term bindings of proof context"
+    (Pretty.string_of o Pretty.chunks o Proof_Context.pretty_binds o Toplevel.context_of);
+
+val _ =
+  register "facts" "facts of proof context"
     (fn st =>
       Proof_Context.pretty_local_facts (Toplevel.context_of st) false
       |> Pretty.chunks |> Pretty.string_of);
 
+val _ =
+  register "state" "proof state"
+    (Pretty.string_of o Pretty.chunks o Toplevel.pretty_state true);
+
 end;