src/Pure/Isar/toplevel.ML
changeset 44186 806f0ec1a43d
parent 44185 05641edb5d30
child 44187 88d770052bac
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Aug 13 20:20:36 2011 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Aug 13 20:41:29 2011 +0200
     1.3 @@ -45,9 +45,8 @@
     1.4    val set_print: bool -> transition -> transition
     1.5    val print: transition -> transition
     1.6    val no_timing: transition -> transition
     1.7 -  val init_theory: Path.T option -> string -> (Path.T option -> theory) -> transition -> transition
     1.8 -  val modify_master: Path.T option -> transition -> transition
     1.9 -  val modify_init: (Path.T option -> theory) -> transition -> transition
    1.10 +  val init_theory: string -> (unit -> theory) -> transition -> transition
    1.11 +  val modify_init: (unit -> theory) -> transition -> transition
    1.12    val exit: transition -> transition
    1.13    val keep: (state -> unit) -> transition -> transition
    1.14    val keep': (bool -> state -> unit) -> transition -> transition
    1.15 @@ -297,16 +296,16 @@
    1.16  (* primitive transitions *)
    1.17  
    1.18  datatype trans =
    1.19 -  Init of Path.T option * string * (Path.T option -> theory) | (*master dir, theory name, init*)
    1.20 +  Init of string * (unit -> theory) | (*theory name, init*)
    1.21    Exit |                                 (*formal exit of theory*)
    1.22    Keep of bool -> state -> unit |        (*peek at state*)
    1.23    Transaction of (bool -> node -> node) * (state -> unit);  (*node transaction and presentation*)
    1.24  
    1.25  local
    1.26  
    1.27 -fun apply_tr _ (Init (master, _, f)) (State (NONE, _)) =
    1.28 +fun apply_tr _ (Init (_, f)) (State (NONE, _)) =
    1.29        State (SOME (Theory (Context.Theory
    1.30 -          (Theory.checkpoint (Runtime.controlled_execution f master)), NONE)), NONE)
    1.31 +          (Theory.checkpoint (Runtime.controlled_execution f ())), NONE)), NONE)
    1.32    | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
    1.33        exit_transaction state
    1.34    | apply_tr int (Keep f) state =
    1.35 @@ -398,16 +397,11 @@
    1.36  
    1.37  (* basic transitions *)
    1.38  
    1.39 -fun init_theory master name f = add_trans (Init (master, name, f));
    1.40 -
    1.41 -fun modify_master master tr =
    1.42 -  (case get_init tr of
    1.43 -    SOME (_, name, f) => init_theory master name f (reset_trans tr)
    1.44 -  | NONE => tr);
    1.45 +fun init_theory name f = add_trans (Init (name, f));
    1.46  
    1.47  fun modify_init f tr =
    1.48    (case get_init tr of
    1.49 -    SOME (master, name, _) => init_theory master name f (reset_trans tr)
    1.50 +    SOME (name, _) => init_theory name f (reset_trans tr)
    1.51    | NONE => tr);
    1.52  
    1.53  val exit = add_trans Exit;