Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Improved error reporting when activating a locale instance (beyond syntax decls).
authorballarin
Sat, 24 Jun 2017 17:44:26 +0200
changeset 66188 bd841164592f
parent 66187 85925d4ae93d
child 66189 23917e861eaa
Improved error reporting when activating a locale instance (beyond syntax decls).
src/Pure/Isar/locale.ML file | annotate | diff | comparison | revisions 
--- 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) =
isabelle