# HG changeset patch
# User wenzelm
# Date 1399452139 -7200
# Node ID 62d237cdc341aecf7014b155b55aa492b7bc384b
# Parent  1c7552b05466b5a19114da08dae12f957f30e82e
tuned;

diff -r 1c7552b05466 -r 62d237cdc341 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed May 07 10:27:20 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed May 07 10:42:19 2014 +0200
@@ -792,8 +792,9 @@
       Toplevel.keep (Attrib.print_options o Toplevel.context_of)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_context"} "print main context"
-    (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_state_context)));
+  Outer_Syntax.improper_command @{command_spec "print_context"}
+    "print context of local theory target"
+    (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_theory"}
diff -r 1c7552b05466 -r 62d237cdc341 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed May 07 10:27:20 2014 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed May 07 10:42:19 2014 +0200
@@ -22,7 +22,7 @@
   val proof_of: state -> Proof.state
   val proof_position_of: state -> int
   val end_theory: Position.T -> state -> theory
-  val pretty_state_context: state -> Pretty.T list
+  val pretty_context: state -> Pretty.T list
   val pretty_state: state -> Pretty.T list
   val print_state: state -> unit
   val pretty_abstract: state -> Pretty.T
@@ -198,14 +198,18 @@
 
 (* print state *)
 
-val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.theory_init) I;
-
-fun pretty_state_context state =
+fun pretty_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);
+  | SOME node =>
+      let
+        val gthy =
+          (case node of
+            Theory (gthy, _) => gthy
+          | Proof (_, (_, gthy)) => gthy
+          | Skipped_Proof (_, (gthy, _)) => gthy);
+        val lthy = Context.cases (Named_Target.theory_init) I gthy;
+      in Local_Theory.pretty lthy end);
 
 fun pretty_state state =
   (case try node_of state of
diff -r 1c7552b05466 -r 62d237cdc341 src/Pure/Tools/print_operation.ML
--- a/src/Pure/Tools/print_operation.ML	Wed May 07 10:27:20 2014 +0200
+++ b/src/Pure/Tools/print_operation.ML	Wed May 07 10:42:19 2014 +0200
@@ -61,8 +61,8 @@
 (* common print operations *)
 
 val _ =
-  register "context" "main context"
-    (Pretty.string_of o Pretty.chunks o Toplevel.pretty_state_context);
+  register "context" "context of local theory target"
+    (Pretty.string_of o Pretty.chunks o Toplevel.pretty_context);
 
 val _ =
   register "cases" "cases of proof context"