# HG changeset patch
# User wenzelm
# Date 1376679495 -7200
# Node ID d51bac27d4a0ad86aaddfffb3118a13fdcd6b404
# Parent  e6edd7abc4ceb698c3909ebfabfdf2e4666bebd2
more markup -- avoid old Locale.extern;
removed obsolete Locale.intern -- prefer Locale.check;

diff -r e6edd7abc4ce -r d51bac27d4a0 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Aug 16 19:03:31 2013 +0200
+++ b/src/Pure/Isar/expression.ML	Fri Aug 16 20:58:15 2013 +0200
@@ -89,6 +89,8 @@
 
 fun parameters_of thy strict (expr, fixed) =
   let
+    val ctxt = Proof_Context.init_global thy;
+
     fun reject_dups message xs =
       (case duplicates (op =) xs of
         [] => ()
@@ -103,16 +105,18 @@
             val ps = params_loc loc;
             val d = length ps - length insts;
             val insts' =
-              if d < 0 then error ("More arguments than parameters in instantiation of locale " ^
-                quote (Locale.extern thy loc))
+              if d < 0 then
+                error ("More arguments than parameters in instantiation of locale " ^
+                  quote (Locale.markup_name ctxt loc))
               else insts @ replicate d NONE;
             val ps' = (ps ~~ insts') |>
               map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
           in (ps', (loc, (prfx, Positional insts'))) end
       | params_inst (loc, (prfx, Named insts)) =
           let
-            val _ = reject_dups "Duplicate instantiation of the following parameter(s): "
-              (map fst insts);
+            val _ =
+              reject_dups "Duplicate instantiation of the following parameter(s): "
+                (map fst insts);
             val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps =>
               if AList.defined (op =) ps p then AList.delete (op =) p ps
               else error (quote p ^ " not a parameter of instantiated expression"));
diff -r e6edd7abc4ce -r d51bac27d4a0 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Aug 16 19:03:31 2013 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Aug 16 20:58:15 2013 +0200
@@ -36,9 +36,9 @@
     declaration list ->
     (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list ->
     (string * morphism) list -> theory -> theory
-  val intern: theory -> xstring -> string
   val check: theory -> xstring * Position.T -> string
   val extern: theory -> string -> xstring
+  val markup_name: Proof.context -> string -> string
   val pretty_name: Proof.context -> string -> Pretty.T
   val defined: theory -> string -> bool
   val params_of: theory -> string -> ((string * typ) * mixfix) list
@@ -159,13 +159,15 @@
   val merge = Name_Space.join_tables (K merge_locale);
 );
 
-val intern = Name_Space.intern o #1 o Locales.get;
 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);
+fun markup_extern ctxt =
+  Name_Space.markup_extern ctxt (#1 (Locales.get (Proof_Context.theory_of ctxt)));
+
+fun markup_name ctxt name = markup_extern ctxt name |-> Markup.markup;
+fun pretty_name ctxt name = markup_extern ctxt name |> Pretty.mark_str;
 
 val get_locale = Symtab.lookup o #2 o Locales.get;
 val defined = Symtab.defined o #2 o Locales.get;
@@ -207,7 +209,7 @@
 fun mixins_of thy name serial = the_locale thy name |>
   #mixins |> lookup_mixins serial;
 
-(* FIXME unused *)
+(* FIXME unused!? *)
 fun identity_on thy name morph =
   let val mk_instance = instance_of thy name
   in ListPair.all Term.aconv_untyped (mk_instance Morphism.identity, mk_instance morph) end;
@@ -462,15 +464,18 @@
 fun amend_registration (name, morph) mixin export context =
   let
     val thy = Context.theory_of context;
+    val ctxt = Context.proof_of context;
+
     val regs = Registrations.get context |> fst;
     val base = instance_of thy name (morph $> export);
-    val serial' = case Idtab.lookup regs (name, base) of
+    val serial' =
+      (case Idtab.lookup regs (name, base) of
         NONE =>
-          error ("No interpretation of locale " ^
-            quote (extern thy name) ^ " with\nparameter instantiation " ^
+          error ("No interpretation of locale " ^ quote (markup_name ctxt name) ^
+            " with\nparameter instantiation " ^
             space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
             " available")
-      | SOME (_, serial') => serial';
+      | SOME (_, serial') => serial');
   in
     add_mixin serial' mixin context
   end;
@@ -502,7 +507,7 @@
 
 (*** Dependencies ***)
 
-(*
+(* FIXME dead code!?
 fun amend_dependency loc (name, morph) mixin export thy =
   let
     val deps = dependencies_of thy loc;