changeset 68538 | 0903c4c8b455 |
parent 68381 | 2fd3a6d6ba2e |
child 68866 | d4681a748873 |
--- 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;