# HG changeset patch # User wenzelm # Date 1430668347 -7200 # Node ID 79ad597fe699908cce0fed2554f1a52f71a18653 # Parent 523ec7e4b02283c9b5bbaf2dd45653cc3c22bd60 tuned output; diff -r 523ec7e4b022 -r 79ad597fe699 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Sun May 03 17:41:54 2015 +0200 +++ b/src/Pure/Isar/toplevel.ML Sun May 03 17:52:27 2015 +0200 @@ -382,9 +382,9 @@ val lthy = f thy; val gthy = if begin then Context.Proof lthy else Context.Theory (Named_Target.exit lthy); val _ = - if begin then - Output.state (Pretty.string_of (Pretty.chunks (Local_Theory.pretty lthy))) - else (); + (case Local_Theory.pretty lthy of + [] => () + | prts => Output.state (Pretty.string_of (Pretty.chunks prts))); in Theory (gthy, SOME lthy) end | _ => raise UNDEF));