# HG changeset patch # User wenzelm # Date 1275294462 -7200 # Node ID 1509e49c8d33c48cf529738fee7ed5fef5709394 # Parent 12d850a27eefc29626cdd3cd768d395e19c82392 Theory_Target.pretty: more markup; diff -r 12d850a27eef -r 1509e49c8d33 src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Mon May 31 10:24:21 2010 +0200 +++ b/src/Pure/Isar/theory_target.ML Mon May 31 10:27:42 2010 +0200 @@ -50,7 +50,9 @@ fun pretty_thy ctxt target is_class = let val thy = ProofContext.theory_of ctxt; - val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target; + val target_name = + [Pretty.command (if is_class then "class" else "locale"), + Pretty.str (" " ^ Locale.extern thy target)]; val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt)); val assumes = @@ -60,13 +62,13 @@ (if null assumes then [] else [Element.Assumes assumes]); in if target = "" then [] - else if null elems then [Pretty.str target_name] - else [Pretty.big_list (target_name ^ " =") - (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)] + else if null elems then [Pretty.block target_name] + else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) :: + map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))] end; fun pretty (Target {target, is_class, instantiation, overloading, ...}) ctxt = - Pretty.block [Pretty.str "theory", Pretty.brk 1, + Pretty.block [Pretty.command "theory", Pretty.brk 1, Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] :: (if not (null overloading) then [Overloading.pretty ctxt] else if not (null (#1 instantiation)) then [Class_Target.pretty_instantiation ctxt]