# HG changeset patch
# User wenzelm
# Date 1399300219 -7200
# Node ID 2241091050084596ec4e689c9723e5aa1e0bc9c0
# Parent  c4512e94e15c467b027ded15259a4dbf461eeb81
more print operations;
preserve declaration order;

diff -r c4512e94e15c -r 224109105008 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon May 05 16:29:09 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon May 05 16:30:19 2014 +0200
@@ -788,7 +788,7 @@
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_context"} "print main context"
-    (Scan.succeed (Toplevel.keep Toplevel.print_state_context));
+    (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_state_context)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_theory"}
@@ -905,7 +905,7 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_binds"} "print term bindings of proof context"
     (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (Proof_Context.print_binds o Toplevel.context_of)));
+      Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_binds o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_facts"} "print facts of proof context"
@@ -915,7 +915,7 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_cases"} "print cases of proof context"
     (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (Proof_Context.print_cases o Toplevel.context_of)));
+      Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_statement"}
diff -r c4512e94e15c -r 224109105008 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon May 05 16:29:09 2014 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon May 05 16:30:19 2014 +0200
@@ -161,10 +161,10 @@
   val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic
   val print_syntax: Proof.context -> unit
   val print_abbrevs: Proof.context -> unit
-  val print_binds: Proof.context -> unit
+  val pretty_binds: Proof.context -> Pretty.T list
   val pretty_local_facts: Proof.context -> bool -> Pretty.T list
   val print_local_facts: Proof.context -> bool -> unit
-  val print_cases: Proof.context -> unit
+  val pretty_cases: Proof.context -> Pretty.T list
   val debug: bool Config.T
   val verbose: bool Config.T
   val pretty_ctxt: Proof.context -> Pretty.T list
@@ -1266,8 +1266,6 @@
     else [Pretty.big_list "term bindings:" (map prt_bind (Vartab.dest binds))]
   end;
 
-val print_binds = Pretty.writeln_chunks o pretty_binds;
-
 
 (* local facts *)
 
@@ -1333,8 +1331,6 @@
     else [Pretty.big_list "cases:" (map pretty_case cases)]
   end;
 
-val print_cases = Pretty.writeln_chunks o pretty_cases;
-
 end;
 
 
diff -r c4512e94e15c -r 224109105008 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon May 05 16:29:09 2014 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon May 05 16:30:19 2014 +0200
@@ -22,7 +22,8 @@
   val proof_of: state -> Proof.state
   val proof_position_of: state -> int
   val end_theory: Position.T -> state -> theory
-  val print_state_context: state -> unit
+  val pretty_state_context: state -> Pretty.T list
+  val pretty_state: bool -> state -> Pretty.T list
   val print_state: bool -> state -> unit
   val pretty_abstract: state -> Pretty.T
   val quiet: bool Unsynchronized.ref
@@ -199,22 +200,23 @@
 
 val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.theory_init) I;
 
-fun print_state_context state =
+fun pretty_state_context state =
   (case try node_of state of
     NONE => []
   | SOME (Theory (gthy, _)) => pretty_context gthy
   | SOME (Proof (_, (_, gthy))) => pretty_context gthy
-  | SOME (Skipped_Proof (_, (gthy, _))) => pretty_context gthy)
-  |> Pretty.writeln_chunks;
+  | SOME (Skipped_Proof (_, (gthy, _))) => pretty_context gthy);
 
-fun print_state prf_only state =
+fun pretty_state prf_only state =
   (case try node_of state of
     NONE => []
   | SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy
   | SOME (Proof (prf, _)) =>
       Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
-  | SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)])
-  |> Pretty.markup_chunks Markup.state |> Pretty.writeln;
+  | SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]);
+
+fun print_state prf_only =
+  pretty_state prf_only #> Pretty.markup_chunks Markup.state #> Pretty.writeln;
 
 fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
 
diff -r c4512e94e15c -r 224109105008 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;