src/Pure/PIDE/document.ML
changeset 44270 3eaad39e520c
parent 44247 270366301bd7
child 44271 89f40a5939b2
--- a/src/Pure/PIDE/document.ML	Thu Aug 18 17:30:47 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Aug 18 17:53:32 2011 +0200
@@ -268,7 +268,7 @@
       (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
         [] => Exn.interrupt ()
       | errs => (errs, NONE))
-  | NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE));
+  | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));
 
 in