# HG changeset patch
# User ballarin
# Date 1498319066 -7200
# Node ID bd841164592f31fcb6601602e5e99f6a540470e3
# Parent  85925d4ae93d7e8663e288a6022c5de9372ec8bf
Improved error reporting when activating a locale instance (beyond syntax decls).

diff -r 85925d4ae93d -r bd841164592f src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Jun 24 17:42:50 2017 +0200
+++ b/src/Pure/Isar/locale.ML	Sat Jun 24 17:44:26 2017 +0200
@@ -432,8 +432,10 @@
       grouped 100 Par_List.map
         (Element.transform_ctxt morph' o Notes o #1) (#notes (the_locale thy name));
   in
-    fold_rev (fn elem => fn res => activ_elem (Element.transform_ctxt (transfer res) elem) res)
-      notes' input
+    input
+    |> fold_rev
+        (fn elem => fn res => activ_elem (Element.transform_ctxt (transfer res) elem) res) notes'
+      handle ERROR msg => activate_err msg (name, morph) context
   end;
 
 fun activate_all name thy activ_elem transfer (marked, input) =