# HG changeset patch
# User wenzelm
# Date 1530273734 -7200
# Node ID 0903c4c8b4556aa6d38d29e36fbb8ef8d6203e96
# Parent  0299c1dccc961c0c1467c756a6ffd685ddab1d99
always consolidate: allow errors in presentation;

diff -r 0299c1dccc96 -r 0903c4c8b455 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;