always consolidate: allow errors in presentation;
authorwenzelm
Fri, 29 Jun 2018 14:02:14 +0200
changeset 68538 0903c4c8b455
parent 68537 0299c1dccc96
child 68539 6740e3611a86
always consolidate: allow errors in presentation;
src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Jun 29 11:36:31 2018 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Jun 29 14:02:14 2018 +0200
@@ -735,8 +735,9 @@
                     segments = segments};
                 in
                   fn _ =>
-                    (Thy_Info.apply_presentation presentation_context thy;
-                     commit_consolidated node)
+                    Exn.release
+                      (Exn.capture (Thy_Info.apply_presentation presentation_context) thy
+                        before commit_consolidated node)
                 end
               else fn _ => commit_consolidated node;