recovered outer Pretty.block from 30c1639a343a, avoid excessive line breaks due to implicit Pretty.chunks;
authorwenzelm
Thu, 15 Feb 2018 14:36:46 +0100
changeset 67615 967213048e55
parent 67614 560fbd6bc047
child 67617 9f9f64fe1705
child 67618 3107dcea3493
child 67621 8f93d878f855
recovered outer Pretty.block from 30c1639a343a, avoid excessive line breaks due to implicit Pretty.chunks;
src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Thu Feb 15 13:04:36 2018 +0100
+++ b/src/Pure/Isar/named_target.ML	Thu Feb 15 14:36:46 2018 +0100
@@ -104,7 +104,8 @@
        declaration = Generic_Target.locale_declaration locale,
        theory_registration = fn _ => error "Not possible in locale target",
        locale_dependency = Generic_Target.locale_dependency locale,
-       pretty = fn ctxt => Locale.pretty_locale (Proof_Context.theory_of ctxt) false locale}
+       pretty = fn ctxt =>
+        [Pretty.block (Locale.pretty_locale (Proof_Context.theory_of ctxt) false locale)]}
   | operations (Class class) =
       {define = Generic_Target.define (class_foundation class),
        notes = Generic_Target.notes (Generic_Target.locale_target_notes class),