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