# HG changeset patch
# User wenzelm
# Date 1537795221 -7200
# Node ID 480d60d3c5ef67fec3f45395360bb60d01170c70
# Parent  cc5d5d9f9a4bba7184928723ef525d755e9a4be4
more position information;
tuned;

diff -r cc5d5d9f9a4b -r 480d60d3c5ef src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Sep 24 14:58:15 2018 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Sep 24 15:20:21 2018 +0200
@@ -334,7 +334,7 @@
 val total_ident_ord = prod_ord fast_string_ord (list_ord Term_Ord.fast_term_ord);
 structure Idtab = Table(type key = string * term list val ord = total_ident_ord);
 
-type reg = {morphisms: morphism * morphism, serial: serial};
+type reg = {morphisms: morphism * morphism, pos: Position.T, serial: serial};
 type regs = reg Idtab.table;
 
 val join_regs : regs * regs -> regs =
@@ -356,16 +356,18 @@
         handle Idtab.DUP id =>
           (*distinct interpretations with same base: merge their mixins*)
           let
-            val ctxt1 = Syntax.init_pretty_global (#1 old_thys);
-            val serial1 = #serial (Idtab.lookup regs1 id |> the);
-
+            val reg1 = Idtab.lookup regs1 id |> the;
             val reg2 = Idtab.lookup regs2 id |> the;
-            val regs2' = Idtab.update (id, {morphisms = #morphisms reg2, serial = serial1}) regs2;
-            val mixins2' = rename_mixin (#serial reg2, serial1) mixins2;
+            val reg2' =
+             {morphisms = #morphisms reg2,
+              pos = Position.thread_data (),
+              serial = #serial reg1};
+            val regs2' = Idtab.update (id, reg2') regs2;
+            val mixins2' = rename_mixin (#serial reg2, #serial reg1) mixins2;
             val _ =
-              (warning o Pretty.string_of o Pretty.block)
-                [Pretty.str "Removed duplicate interpretation (after retrieving its mixins):",
-                  Pretty.brk 1, pretty_reg_inst ctxt1 [] id];
+              warning ("Removed duplicate interpretation after retrieving its mixins" ^
+                Position.here_list [#pos reg1, #pos reg2] ^ ":\n  " ^
+                Pretty.string_of (pretty_reg_inst (Syntax.init_pretty_global (#1 old_thys)) [] id));
           in recursive_merge ((regs1, mixins1), (regs2', mixins2')) end;
     in recursive_merge end;
 );
@@ -386,7 +388,7 @@
 
 fun add_reg thy export (name, morph) =
   let
-    val reg = {morphisms = (morph, export), serial = serial ()};
+    val reg = {morphisms = (morph, export), pos = Position.thread_data (), serial = serial ()};
     val id = (name, instance_of thy name (morph $> export));
   in (map_registrations o apfst) (Idtab.insert (K false) (id, reg)) end;