# HG changeset patch
# User wenzelm
# Date 1399463716 -7200
# Node ID c668735fb8b56a90a729fbfe7cd44529b524d76f
# Parent  1e3c3df3a77cedabcdc6f5082978c36c88e46fe8
print results as "state", to avoid intrusion into the source text;
print new local theory (again);

diff -r 1e3c3df3a77c -r c668735fb8b5 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Wed May 07 13:25:54 2014 +0200
+++ b/src/Pure/Isar/obtain.ML	Wed May 07 13:55:16 2014 +0200
@@ -300,7 +300,7 @@
 
     val goal = Var (("guess", 0), propT);
     fun print_result ctxt' (k, [(s, [_, th])]) =
-      Proof_Display.print_results Markup.state int ctxt' (k, [(s, [th])]);
+      Proof_Display.print_results int ctxt' (k, [(s, [th])]);
     val before_qed =
       Method.primitive_text (fn ctxt =>
         Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #>
diff -r 1e3c3df3a77c -r c668735fb8b5 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed May 07 13:25:54 2014 +0200
+++ b/src/Pure/Isar/proof.ML	Wed May 07 13:55:16 2014 +0200
@@ -1042,7 +1042,7 @@
 local
 
 fun gen_have prep_att prepp before_qed after_qed stmt int =
-  local_goal (Proof_Display.print_results Markup.state int)
+  local_goal (Proof_Display.print_results int)
     prep_att prepp "have" before_qed after_qed stmt;
 
 fun gen_show prep_att prepp before_qed after_qed stmt int state =
@@ -1056,7 +1056,7 @@
 
     fun print_results ctxt res =
       if ! testing then ()
-      else Proof_Display.print_results Markup.state int ctxt res;
+      else Proof_Display.print_results int ctxt res;
     fun print_rule ctxt th =
       if ! testing then rule := SOME th
       else if int then
diff -r 1e3c3df3a77c -r c668735fb8b5 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Wed May 07 13:25:54 2014 +0200
+++ b/src/Pure/Isar/proof_display.ML	Wed May 07 13:55:16 2014 +0200
@@ -22,8 +22,7 @@
   val pretty_goal_facts: Proof.context -> string -> thm list -> Pretty.T
   val method_error: string -> Position.T ->
     {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
-  val print_results: Markup.T -> bool -> Proof.context ->
-    ((string * string) * (string * thm list) list) -> unit
+  val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit
   val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit
 end
 
@@ -141,13 +140,13 @@
 
 in
 
-fun print_results markup do_print ctxt ((kind, name), facts) =
+fun print_results do_print ctxt ((kind, name), facts) =
   if not do_print orelse kind = "" then ()
   else if name = "" then
-    (Output.urgent_message o Pretty.string_of o Pretty.mark markup)
+    (Pretty.writeln o Pretty.mark Markup.state)
       (Pretty.block (Pretty.keyword1 kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
   else
-    (Output.urgent_message o Pretty.string_of o Pretty.mark markup)
+    (Pretty.writeln o Pretty.mark Markup.state)
       (case facts of
         [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
           Proof_Context.pretty_fact ctxt fact])
@@ -176,7 +175,7 @@
 
 fun print_consts do_print ctxt pred cs =
   if not do_print orelse null cs then ()
-  else Pretty.writeln (pretty_consts ctxt pred cs);
+  else Pretty.writeln (Pretty.mark Markup.state (pretty_consts ctxt pred cs));
 
 end;
 
diff -r 1e3c3df3a77c -r c668735fb8b5 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed May 07 13:25:54 2014 +0200
+++ b/src/Pure/Isar/specification.ML	Wed May 07 13:55:16 2014 +0200
@@ -301,7 +301,7 @@
       |> Attrib.partial_evaluation ctxt'
       |> Element.transform_facts (Proof_Context.export_morphism ctxt' lthy);
     val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts';
-    val _ = Proof_Display.print_results Markup.empty int lthy' ((kind, ""), res);
+    val _ = Proof_Display.print_results int lthy' ((kind, ""), res);
   in (res, lthy') end;
 
 in
@@ -400,12 +400,12 @@
               (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;
         val lthy'' =
           if Attrib.is_empty_binding (name, atts) then
-            (Proof_Display.print_results Markup.empty int lthy' ((kind, ""), res); lthy')
+            (Proof_Display.print_results int lthy' ((kind, ""), res); lthy')
           else
             let
               val ([(res_name, _)], lthy'') =
                 Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy';
-              val _ = Proof_Display.print_results Markup.empty int lthy' ((kind, res_name), res);
+              val _ = Proof_Display.print_results int lthy' ((kind, res_name), res);
             in lthy'' end;
       in after_qed results' lthy'' end;
   in
diff -r 1e3c3df3a77c -r c668735fb8b5 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed May 07 13:25:54 2014 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed May 07 13:55:16 2014 +0200
@@ -409,6 +409,10 @@
         let
           val lthy = f thy;
           val gthy = if begin then Context.Proof lthy else Context.Theory (loc_exit lthy);
+          val _ =
+            if begin then
+              Pretty.writeln (Pretty.mark Markup.state (Pretty.chunks (Local_Theory.pretty lthy)))
+            else ();
         in Theory (gthy, SOME lthy) end
     | _ => raise UNDEF));