# HG changeset patch # User wenzelm # Date 1399666446 -7200 # Node ID b47193851dc6993c81241efdea87aa7d675d0229 # Parent 11a4001b06c6bd1a7e7eb0023096b13c8d3348f9 more markup; diff -r 11a4001b06c6 -r b47193851dc6 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Fri May 09 22:04:50 2014 +0200 +++ b/src/Pure/Isar/proof.ML Fri May 09 22:14:06 2014 +0200 @@ -1064,7 +1064,10 @@ fun print_rule ctxt th = if ! testing then rule := SOME th else if int then - writeln (Markup.markup Markup.state (Proof_Display.string_of_rule ctxt "Successful" th)) + Proof_Display.string_of_rule ctxt "Successful" th + |> Markup.markup Markup.text_fold + |> Markup.markup Markup.state + |> writeln else (); val test_proof = local_skip_proof true