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