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