--- 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;
--- 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])