Improved error reporting when activating a locale instance.
--- 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 =