1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Nov 15 18:31:53 2007 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Nov 18 16:10:11 2007 +0100
     1.3 @@ -57,7 +57,7 @@
     1.4    val no_timing: transition -> transition
     1.5    val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit) ->
     1.6      transition -> transition
     1.7 -  val init_empty: (unit -> unit) -> transition -> transition
     1.8 +  val init_empty: (state -> bool) -> (unit -> unit) -> transition -> transition
     1.9    val exit: transition -> transition
    1.10    val undo_exit: transition -> transition
    1.11    val kill: transition -> transition
    1.12 @@ -389,7 +389,7 @@
    1.13  datatype trans =
    1.14    Init of (bool -> theory) * ((theory -> unit) * (theory -> unit)) |
    1.15                                                      (*init node; with exit/kill operation*)
    1.16 -  InitEmpty of unit -> unit |                       (*init empty toplevel*)
    1.17 +  InitEmpty of (state -> bool) * (unit -> unit) |   (*init empty toplevel*)
    1.18    Exit |                                            (*conclude node -- deferred until init*)
    1.19    UndoExit |                                        (*continue after conclusion*)
    1.20    Kill |                                            (*abort node*)
    1.21 @@ -412,8 +412,9 @@
    1.22  fun apply_tr int _ (Init (f, term)) (state as Toplevel _) =
    1.23        let val node = Theory (Context.Theory (f int), NONE)
    1.24        in safe_exit state; State (History.init (undo_limit int) node, term) end
    1.25 -  | apply_tr int _ (InitEmpty f) (state as Toplevel _) =
    1.26 -      (safe_exit state; keep_state int (fn _ => fn _ => f ()) toplevel)
    1.27 +  | apply_tr int _ (InitEmpty (check, f)) (state as Toplevel _) =
    1.28 +      if check state then (safe_exit state; keep_state int (fn _ => fn _ => f ()) toplevel)
    1.29 +      else raise UNDEF
    1.30    | apply_tr _ _ Exit (State (node, term)) =
    1.31        (the_global_theory (History.current node); Toplevel (SOME (node, term)))
    1.32    | apply_tr _ _ UndoExit (Toplevel (SOME state_info)) = State state_info
    1.33 @@ -508,7 +509,7 @@
    1.34  (* basic transitions *)
    1.35  
    1.36  fun init_theory f exit kill = add_trans (Init (f, (exit, kill)));
    1.37 -val init_empty = add_trans o InitEmpty;
    1.38 +fun init_empty check f = add_trans (InitEmpty (check, f));
    1.39  val exit = add_trans Exit;
    1.40  val undo_exit = add_trans UndoExit;
    1.41  val kill = add_trans Kill;
    1.42 @@ -741,7 +742,7 @@
    1.43  fun >>> [] = ()
    1.44    | >>> (tr :: trs) = if >> tr then >>> trs else ();
    1.45  
    1.46 -fun init_state () = (>> (init_empty (K ()) empty); ());
    1.47 +fun init_state () = (>> (init_empty (K true) (K ()) empty); ());
    1.48  
    1.49  
    1.50  (* the Isar source of transitions *)