# HG changeset patch
# User wenzelm
# Date 1369151153 -7200
# Node ID fb577a13abbdb513ee4c8bdf0d9b2bf3a9b14a62
# Parent  59cc8881e911d6458e0f37c3c43dd80f4cf0eb1e
more markup;

diff -r 59cc8881e911 -r fb577a13abbd src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue May 21 16:51:16 2013 +0200
+++ b/src/Pure/Isar/locale.ML	Tue May 21 17:45:53 2013 +0200
@@ -39,6 +39,7 @@
   val intern: theory -> xstring -> string
   val check: theory -> xstring * Position.T -> string
   val extern: theory -> string -> xstring
+  val pretty_name: Proof.context -> string -> Pretty.T
   val defined: theory -> string -> bool
   val params_of: theory -> string -> ((string * typ) * mixfix) list
   val intros_of: theory -> string -> thm option * thm option
@@ -162,6 +163,10 @@
 fun check thy = #1 o Name_Space.check (Context.Theory thy) (Locales.get thy);
 fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (#1 (Locales.get thy));
 
+fun pretty_name ctxt name =
+  Pretty.mark_str
+    (Name_Space.markup_extern ctxt (#1 (Locales.get (Proof_Context.theory_of ctxt))) name);
+
 val get_locale = Symtab.lookup o #2 o Locales.get;
 val defined = Symtab.defined o #2 o Locales.get;
 
@@ -212,7 +217,6 @@
 fun pretty_reg ctxt export (name, morph) =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val name' = extern thy name;
     val morph' = morph $> export;
     fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
     fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
@@ -223,7 +227,7 @@
         Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
       else prt_term t;
     fun prt_inst ts =
-      Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts));
+      Pretty.block (Pretty.breaks (pretty_name ctxt name :: map prt_term' ts));
 
     val qs = Binding.name "x" |> Morphism.binding morph' |> Binding.prefix_of;
     val ts = instance_of thy name morph';
@@ -620,7 +624,7 @@
 
 fun pretty_locale thy show_facts name =
   let
-    val ctxt = init name thy;
+    val locale_ctxt = init name thy;
     fun cons_elem (elem as Notes _) = show_facts ? cons elem
       | cons_elem elem = cons elem;
     val elems =
@@ -628,8 +632,8 @@
       |> snd |> rev;
   in
     Pretty.block
-      (Pretty.command "locale" :: Pretty.brk 1 :: Pretty.str (extern thy name) ::
-        maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt ctxt elem)]) elems)
+      (Pretty.command "locale" :: Pretty.brk 1 :: pretty_name locale_ctxt name ::
+        maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt locale_ctxt elem)]) elems)
   end;
 
 fun print_locale thy show_facts raw_name =
diff -r 59cc8881e911 -r fb577a13abbd src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Tue May 21 16:51:16 2013 +0200
+++ b/src/Pure/Isar/named_target.ML	Tue May 21 17:45:53 2013 +0200
@@ -124,10 +124,9 @@
 
 fun pretty (Target {target, is_locale, is_class, ...}) ctxt =
   let
-    val thy = Proof_Context.theory_of ctxt;
     val target_name =
-      [Pretty.command (if is_class then "class" else "locale"),
-        Pretty.str (" " ^ Locale.extern thy target)];
+      [Pretty.command (if is_class then "class" else "locale"), Pretty.brk 1,
+        Locale.pretty_name ctxt target];
     val fixes =
       map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
         (#1 (Proof_Context.inferred_fixes ctxt));