src/Pure/Isar/toplevel.ML
changeset 41536 47fef6afe756
parent 40960 9e54eb514a46
child 41673 1c191a39549f
     1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Jan 13 17:30:52 2011 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Jan 13 17:34:45 2011 +0100
     1.3 @@ -45,8 +45,9 @@
     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: string -> (unit -> theory) -> transition -> transition
     1.8 -  val modify_init: (unit -> theory) -> transition -> transition
     1.9 +  val init_theory: Path.T option -> string -> (Path.T option -> theory) -> transition -> transition
    1.10 +  val modify_master: Path.T option -> transition -> transition
    1.11 +  val modify_init: (Path.T option -> 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 @@ -288,16 +289,16 @@
    1.16  (* primitive transitions *)
    1.17  
    1.18  datatype trans =
    1.19 -  Init of string * (unit -> theory) |    (*theory name, init*)
    1.20 +  Init of Path.T option * string * (Path.T option -> theory) | (*master dir, 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 (_, f)) (State (NONE, _)) =
    1.28 +fun apply_tr _ (Init (master, _, f)) (State (NONE, _)) =
    1.29        State (SOME (Theory (Context.Theory
    1.30 -          (Theory.checkpoint (Runtime.controlled_execution f ())), NONE)), NONE)
    1.31 +          (Theory.checkpoint (Runtime.controlled_execution f master)), NONE)), NONE)
    1.32    | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _)), _)) =
    1.33        State (NONE, prev)
    1.34    | apply_tr int (Keep f) state =
    1.35 @@ -344,9 +345,10 @@
    1.36  
    1.37  (* diagnostics *)
    1.38  
    1.39 -fun init_of (Transition {trans = [Init (name, _)], ...}) = SOME name
    1.40 -  | init_of _ = NONE;
    1.41 +fun get_init (Transition {trans = [Init args], ...}) = SOME args
    1.42 +  | get_init _ = NONE;
    1.43  
    1.44 +val init_of = Option.map #2 o get_init;
    1.45  fun print_of (Transition {print, ...}) = print;
    1.46  fun name_of (Transition {name, ...}) = name;
    1.47  fun pos_of (Transition {pos, ...}) = pos;
    1.48 @@ -387,11 +389,16 @@
    1.49  
    1.50  (* basic transitions *)
    1.51  
    1.52 -fun init_theory name f = add_trans (Init (name, f));
    1.53 +fun init_theory master name f = add_trans (Init (master, name, f));
    1.54 +
    1.55 +fun modify_master master tr =
    1.56 +  (case get_init tr of
    1.57 +    SOME (_, name, f) => init_theory master name f (reset_trans tr)
    1.58 +  | NONE => tr);
    1.59  
    1.60  fun modify_init f tr =
    1.61 -  (case init_of tr of
    1.62 -    SOME name => init_theory name f (reset_trans tr)
    1.63 +  (case get_init tr of
    1.64 +    SOME (master, name, _) => init_theory master name f (reset_trans tr)
    1.65    | NONE => tr);
    1.66  
    1.67  val exit = add_trans Exit;