added exception RESTART;
authorwenzelm
Sun Nov 29 13:17:21 1998 +0100 (1998-11-29)
changeset 59908b6de9bd7d72
parent 5989 9670dae0143d
child 5991 832ec852fc4e
added exception RESTART;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sun Nov 29 13:16:47 1998 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Nov 29 13:17:21 1998 +0100
     1.3 @@ -30,6 +30,7 @@
     1.4    val proof_of: state -> Proof.state
     1.5    type transition
     1.6    exception TERMINATE
     1.7 +  exception RESTART
     1.8    exception BREAK of state
     1.9    val empty: transition
    1.10    val name: string -> transition -> transition
    1.11 @@ -133,6 +134,7 @@
    1.12  (** toplevel transitions **)
    1.13  
    1.14  exception TERMINATE;
    1.15 +exception RESTART;
    1.16  exception BREAK of state;
    1.17  exception FAIL of exn * string;
    1.18  
    1.19 @@ -248,6 +250,7 @@
    1.20  fun raised_msg name msg = raised name ^ ": " ^ msg;
    1.21  
    1.22  fun exn_message TERMINATE = "Exit."
    1.23 +  | exn_message RESTART = "Restart."
    1.24    | exn_message (BREAK _) = "Break."
    1.25    | exn_message (FAIL (exn, msg)) = cat_lines [exn_message exn, msg]
    1.26    | exn_message Interrupt = "Interrupt (exec)."
    1.27 @@ -317,6 +320,7 @@
    1.28    Some (transform_interrupt_state (transform_error (app int tr)) state, None)
    1.29      handle
    1.30        TERMINATE => None
    1.31 +    | RESTART => Some (toplevel, None)
    1.32      | FAIL (exn_info as (BREAK break_state, _)) =>
    1.33          Some (append_states break_state state, Some exn_info)
    1.34      | FAIL exn_info => Some (state, Some exn_info)