src/Pure/PIDE/document.ML
changeset 44271 89f40a5939b2
parent 44270 3eaad39e520c
child 44299 061599cb6eb0
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Aug 18 17:53:32 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Aug 18 18:07:40 2011 +0200
     1.3 @@ -264,8 +264,8 @@
     1.4  fun run int tr st =
     1.5    (case Toplevel.transition int tr st of
     1.6      SOME (st', NONE) => ([], SOME st')
     1.7 -  | SOME (_, SOME exn_info) =>
     1.8 -      (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
     1.9 +  | SOME (_, SOME (exn, _)) =>
    1.10 +      (case ML_Compiler.exn_messages exn of
    1.11          [] => Exn.interrupt ()
    1.12        | errs => (errs, NONE))
    1.13    | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));