# HG changeset patch
# User wenzelm
# Date 1399456230 -7200
# Node ID fa12200276bf661a8016eee5348c4b78dc87017e
# Parent  62d237cdc341aecf7014b155b55aa492b7bc384b
more emphatic output for Proof General;

diff -r 62d237cdc341 -r fa12200276bf src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Wed May 07 10:42:19 2014 +0200
+++ b/src/Pure/Isar/calculation.ML	Wed May 07 11:50:30 2014 +0200
@@ -118,9 +118,9 @@
     val ctxt' = Proof.context_of state';
     val _ =
       if int then
-        Pretty.writeln
-          (Proof_Context.pretty_fact ctxt'
-            (Proof_Context.full_name ctxt' (Binding.name calculationN), calc))
+        Proof_Context.pretty_fact ctxt'
+          (Proof_Context.full_name ctxt' (Binding.name calculationN), calc)
+        |> Pretty.string_of |> Output.urgent_message
       else ();
   in state' |> final ? (put_calculation NONE #> Proof.chain_facts calc) end;
 
diff -r 62d237cdc341 -r fa12200276bf src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Wed May 07 10:42:19 2014 +0200
+++ b/src/Pure/Isar/proof_display.ML	Wed May 07 11:50:30 2014 +0200
@@ -144,10 +144,10 @@
 fun print_results markup do_print ctxt ((kind, name), facts) =
   if not do_print orelse kind = "" then ()
   else if name = "" then
-    (Pretty.writeln o Pretty.mark markup)
+    (Output.urgent_message o Pretty.string_of o Pretty.mark markup)
       (Pretty.block (Pretty.keyword1 kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
   else
-    (Pretty.writeln o Pretty.mark markup)
+    (Output.urgent_message o Pretty.string_of o Pretty.mark markup)
       (case facts of
         [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
           Proof_Context.pretty_fact ctxt fact])