--- a/src/Pure/PIDE/document.ML Thu Aug 18 17:53:32 2011 +0200
+++ b/src/Pure/PIDE/document.ML Thu Aug 18 18:07:40 2011 +0200
@@ -264,8 +264,8 @@
fun run int tr st =
(case Toplevel.transition int tr st of
SOME (st', NONE) => ([], SOME st')
- | SOME (_, SOME exn_info) =>
- (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
+ | SOME (_, SOME (exn, _)) =>
+ (case ML_Compiler.exn_messages exn of
[] => Exn.interrupt ()
| errs => (errs, NONE))
| NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));