src/Pure/Isar/toplevel.ML
changeset 59055 5a7157b8e870
parent 59032 f36496364ce1
child 59150 71b416020f42
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Nov 26 11:43:51 2014 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Nov 26 14:35:55 2014 +0100
     1.3 @@ -80,7 +80,7 @@
     1.4    val add_hook: (transition -> state -> state -> unit) -> unit
     1.5    val get_timing: transition -> Time.time option
     1.6    val put_timing: Time.time option -> transition -> transition
     1.7 -  val transition: bool -> transition -> state -> (state * (exn * string) option) option
     1.8 +  val transition: bool -> transition -> state -> state * (exn * string) option
     1.9    val command_errors: bool -> transition -> state -> Runtime.error list * state option
    1.10    val command_exception: bool -> transition -> state -> state
    1.11    val reset_theory: state -> state option
    1.12 @@ -569,18 +569,12 @@
    1.13  
    1.14  fun transition int tr st =
    1.15    let
    1.16 -    val hooks = get_hooks ();
    1.17 -    fun apply_hooks st' = hooks |> List.app (fn f => (try (fn () => f tr st st') (); ()));
    1.18 -
    1.19 -    val ctxt = try context_of st;
    1.20 -    val res =
    1.21 -      (case app int tr st of
    1.22 -        (_, SOME Runtime.TERMINATE) => NONE
    1.23 -      | (st', SOME (Runtime.EXCURSION_FAIL exn_info)) => SOME (st', SOME exn_info)
    1.24 -      | (st', SOME exn) => SOME (st', SOME (Runtime.exn_context ctxt exn, at_command tr))
    1.25 -      | (st', NONE) => SOME (st', NONE));
    1.26 -    val _ = (case res of SOME (st', NONE) => apply_hooks st' | _ => ());
    1.27 -  in res end;
    1.28 +    val (st', opt_err) = app int tr st;
    1.29 +    val opt_err' = opt_err |> Option.map
    1.30 +      (fn Runtime.EXCURSION_FAIL exn_info => exn_info
    1.31 +        | exn => (Runtime.exn_context (try context_of st) exn, at_command tr));
    1.32 +    val _ = get_hooks () |> List.app (fn f => (try (fn () => f tr st st') (); ()));
    1.33 +  in (st', opt_err') end;
    1.34  
    1.35  end;
    1.36  
    1.37 @@ -589,16 +583,15 @@
    1.38  
    1.39  fun command_errors int tr st =
    1.40    (case transition int tr st of
    1.41 -    SOME (st', NONE) => ([], SOME st')
    1.42 -  | SOME (_, SOME (exn, _)) => (Runtime.exn_messages_ids exn, NONE)
    1.43 -  | NONE => (Runtime.exn_messages_ids Runtime.TERMINATE, NONE));
    1.44 +    (st', NONE) => ([], SOME st')
    1.45 +  | (_, SOME (exn, _)) => (Runtime.exn_messages_ids exn, NONE));
    1.46  
    1.47  fun command_exception int tr st =
    1.48    (case transition int tr st of
    1.49 -    SOME (st', NONE) => st'
    1.50 -  | SOME (_, SOME (exn, info)) =>
    1.51 -      if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)
    1.52 -  | NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
    1.53 +    (st', NONE) => st'
    1.54 +  | (_, SOME (exn, info)) =>
    1.55 +      if Exn.is_interrupt exn then reraise exn
    1.56 +      else raise Runtime.EXCURSION_FAIL (exn, info));
    1.57  
    1.58  val command = command_exception false;
    1.59