print_context;

--- a/src/Pure/Isar/isar_cmd.ML	Fri Aug 20 15:43:25 1999 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Aug 20 15:44:29 1999 +0200
@@ -32,6 +32,7 @@
   val update_thy: string -> Toplevel.transition -> Toplevel.transition
   val update_thy_only: string -> Toplevel.transition -> Toplevel.transition
   val pretty_setmargin: int -> Toplevel.transition -> Toplevel.transition
+  val print_context: Toplevel.transition -> Toplevel.transition
   val print_theory: Toplevel.transition -> Toplevel.transition
   val print_syntax: Toplevel.transition -> Toplevel.transition
   val print_theorems: Toplevel.transition -> Toplevel.transition
@@ -127,8 +128,9 @@
 fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.setmargin n);
 
 
-(* print theory contents *)
+(* print theory *)
 
+val print_context = Toplevel.keep Toplevel.print_state_context;
 val print_theory = Toplevel.keep (PureThy.print_theory o Toplevel.theory_of);
 val print_syntax = Toplevel.keep (Display.print_syntax o Toplevel.theory_of);
 val print_theorems = Toplevel.keep (PureThy.print_theorems o Toplevel.theory_of);

--- a/src/Pure/Isar/isar_syn.ML	Fri Aug 20 15:43:25 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Aug 20 15:44:29 1999 +0200
@@ -440,6 +440,10 @@
   OuterSyntax.improper_command "help" "print outer syntax (global)" K.diag
     (Scan.succeed (Toplevel.imperative OuterSyntax.print_outer_syntax));
 
+val print_contextP =
+  OuterSyntax.improper_command "print_context" "print theory context name" K.diag
+    (Scan.succeed IsarCmd.print_context);
+
 val print_theoryP =
   OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag
     (Scan.succeed IsarCmd.print_theory);
@@ -587,9 +591,10 @@
   skip_proofP, applyP, then_applyP, proofP, alsoP, finallyP, backP,
   cannot_undoP, clear_undoP, redoP, undos_proofP, kill_proofP, undoP,
   (*diagnostic commands*)
-  pretty_setmarginP, print_commandsP, print_theoryP, print_syntaxP,
-  print_attributesP, print_methodsP, print_theoremsP, print_bindsP,
-  print_lthmsP, print_thmsP, print_propP, print_termP, print_typeP,
+  pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
+  print_syntaxP, print_attributesP, print_methodsP, print_theoremsP,
+  print_bindsP, print_lthmsP, print_thmsP, print_propP, print_termP,
+  print_typeP,
   (*system commands*)
   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   touch_thyP, touch_all_thysP, remove_thyP, prP, disable_prP,

--- a/src/Pure/Isar/toplevel.ML	Fri Aug 20 15:43:25 1999 +0200
+++ b/src/Pure/Isar/toplevel.ML	Fri Aug 20 15:44:29 1999 +0200
@@ -12,6 +12,7 @@
   val toplevel: state
   val prompt_state_default: state -> string
   val prompt_state_fn: (state -> string) ref
+  val print_state_context: state -> unit
   val print_state_default: state -> unit
   val print_state_fn: (state -> unit) ref
   val print_state: state -> unit
@@ -74,10 +75,16 @@
 fun str_of_node (Theory _) = "in theory mode"
   | str_of_node (Proof _) = "in proof mode";
 
-fun print_node (Theory thy) = Pretty.writeln (Pretty.block
-      [Pretty.str "Theory:", Pretty.brk 1, Pretty.str (PureThy.get_name thy),
-        Pretty.str " =", Pretty.brk 1, Display.pretty_theory thy])
-  | print_node (Proof prf) = Proof.print_state (ProofHistory.position prf) (ProofHistory.current prf);
+fun print_ctxt thy = Pretty.writeln (Pretty.block
+  [Pretty.str "Theory:", Pretty.brk 1, Pretty.str (PureThy.get_name thy),
+    Pretty.str " =", Pretty.brk 1, Display.pretty_theory thy]);
+
+fun print_node_ctxt (Theory thy) = print_ctxt thy
+  | print_node_ctxt (Proof prf) = print_ctxt (Proof.theory_of (ProofHistory.current prf));
+
+fun print_node (Theory thy) = print_ctxt thy
+  | print_node (Proof prf) = Proof.print_state (ProofHistory.position prf)
+      (ProofHistory.current prf);
 
 
 (* datatype state *)
@@ -100,15 +107,17 @@
 fun prompt_state state = ! prompt_state_fn state;
 
 
-(* print_state hook *)
+(* print state *)
 
-fun print_topnode (State []) = ()
-  | print_topnode (State ((node, _) :: _)) = print_node (History.current node);
+fun print_topnode _ (State []) = ()
+  | print_topnode prt (State ((node, _) :: _)) = prt (History.current node);
+
+val print_state_context = print_topnode print_node_ctxt;
 
 fun print_state_default state =
   let val ref (begin_state, end_state, _) = Goals.current_goals_markers in
     if begin_state = "" then () else writeln begin_state;
-    print_topnode state;
+    print_topnode print_node state;
     if end_state = "" then () else writeln end_state
   end;