src/Pure/Isar/toplevel.ML
changeset 39285 85728a4b5620
parent 39237 be1acdcd55dc
child 39513 fce2202892c4
     1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Sep 09 21:44:52 2010 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Sep 10 23:11:58 2010 +0200
     1.3 @@ -619,7 +619,8 @@
     1.4  fun command tr st =
     1.5    (case transition (! interact) tr st of
     1.6      SOME (st', NONE) => st'
     1.7 -  | SOME (_, SOME exn_info) => raise Runtime.EXCURSION_FAIL exn_info
     1.8 +  | SOME (_, SOME (exn, info)) =>
     1.9 +      if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)
    1.10    | NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
    1.11  
    1.12  fun command_result tr st =