src/Pure/Isar/toplevel.ML
changeset 37977 3ceccd415145
parent 37953 ddc3b72f9a42
child 38236 d8c7be27e01d
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Jul 27 12:59:22 2010 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Jul 27 22:00:26 2010 +0200
     1.3 @@ -46,7 +46,8 @@
     1.4    val interactive: bool -> transition -> transition
     1.5    val print: transition -> transition
     1.6    val no_timing: transition -> transition
     1.7 -  val init_theory: string -> (bool -> theory) -> transition -> transition
     1.8 +  val init_theory: string -> (unit -> theory) -> transition -> transition
     1.9 +  val modify_init: (unit -> theory) -> transition -> transition
    1.10    val exit: transition -> transition
    1.11    val keep: (state -> unit) -> transition -> transition
    1.12    val keep': (bool -> state -> unit) -> transition -> transition
    1.13 @@ -295,16 +296,16 @@
    1.14  (* primitive transitions *)
    1.15  
    1.16  datatype trans =
    1.17 -  Init of string * (bool -> theory) |    (*theory name, init*)
    1.18 +  Init of string * (unit -> theory) |    (*theory name, init*)
    1.19    Exit |                                 (*formal exit of theory*)
    1.20    Keep of bool -> state -> unit |        (*peek at state*)
    1.21    Transaction of (bool -> node -> node) * (state -> unit);  (*node transaction and presentation*)
    1.22  
    1.23  local
    1.24  
    1.25 -fun apply_tr int (Init (_, f)) (State (NONE, _)) =
    1.26 +fun apply_tr _ (Init (_, f)) (State (NONE, _)) =
    1.27        State (SOME (Theory (Context.Theory
    1.28 -          (Theory.checkpoint (Runtime.controlled_execution f int)), NONE)), NONE)
    1.29 +          (Theory.checkpoint (Runtime.controlled_execution f ())), NONE)), NONE)
    1.30    | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _)), _)) =
    1.31        State (NONE, prev)
    1.32    | apply_tr int (Keep f) state =
    1.33 @@ -394,6 +395,12 @@
    1.34  (* basic transitions *)
    1.35  
    1.36  fun init_theory name f = add_trans (Init (name, f));
    1.37 +
    1.38 +fun modify_init f tr =
    1.39 +  (case init_of tr of
    1.40 +    SOME name => init_theory name f (reset_trans tr)
    1.41 +  | NONE => tr);
    1.42 +
    1.43  val exit = add_trans Exit;
    1.44  val keep' = add_trans o Keep;
    1.45