Improved error reporting when activating a locale instance.
authorballarin
Thu, 25 Aug 2016 20:08:40 +0200
changeset 63723 dacc380ab327
parent 63722 b9c8da46443b
child 63724 e7df93d4d9b8
Improved error reporting when activating a locale instance.
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 =