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