# HG changeset patch
# User ballarin
# Date 1472148520 -7200
# Node ID dacc380ab327b506d3ae313150dea53d24389983
# Parent  b9c8da46443b646b68b8fffd0d2bc39cd4ef489e
Improved error reporting when activating a locale instance.

diff -r b9c8da46443b -r dacc380ab327 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Aug 25 17:17:23 2016 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Aug 25 20:08:40 2016 +0200
@@ -403,6 +403,11 @@
 
 (*** Activate context elements of locale ***)
 
+fun activate_err msg (name, morph) context =
+  cat_error msg ("The above error(s) occurred while activating locale instance\n" ^
+    (pretty_reg (Context.proof_of context) Morphism.identity (name, morph) |>
+      Pretty.string_of));
+
 (* Declarations, facts and entire locale content *)
 
 fun activate_syntax_decls (name, morph) context =
@@ -412,6 +417,7 @@
   in
     context
     |> fold_rev (fn (decl, _) => decl morph) syntax_decls
+      handle ERROR msg => activate_err msg (name, morph) context
   end;
 
 fun activate_notes activ_elem transfer context export' (name, morph) input =