Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
authorwenzelm
Thu Jan 13 17:34:45 2011 +0100 (2011-01-13)
changeset 4153647fef6afe756
parent 41535 0112f14d75ec
child 41537 3837045cc8a1
Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/toplevel.ML
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Jan 13 17:30:52 2011 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Jan 13 17:34:45 2011 +0100
     1.3 @@ -30,8 +30,9 @@
     1.4    Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
     1.5      (Thy_Header.args >> (fn (name, imports, uses) =>
     1.6        Toplevel.print o
     1.7 -        Toplevel.init_theory name
     1.8 -          (fn () => Thy_Info.toplevel_begin_theory name imports (map (apfst Path.explode) uses))));
     1.9 +        Toplevel.init_theory NONE name
    1.10 +          (fn master =>
    1.11 +            Thy_Info.toplevel_begin_theory master name imports (map (apfst Path.explode) uses))));
    1.12  
    1.13  val _ =
    1.14    Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Jan 13 17:30:52 2011 +0100
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Jan 13 17:34:45 2011 +0100
     2.3 @@ -31,7 +31,7 @@
     2.4    type isar
     2.5    val isar: TextIO.instream -> bool -> isar
     2.6    val prepare_command: Position.T -> string -> Toplevel.transition
     2.7 -  val load_thy: string -> (unit -> theory) -> Position.T -> string -> (unit -> unit) * theory
     2.8 +  val load_thy: string -> (Path.T option -> theory) -> Position.T -> string -> (unit -> unit) * theory
     2.9  end;
    2.10  
    2.11  structure Outer_Syntax: OUTER_SYNTAX =
    2.12 @@ -204,7 +204,7 @@
    2.13  fun process_file path thy =
    2.14    let
    2.15      val trs = parse (Path.position path) (File.read path);
    2.16 -    val init = Toplevel.init_theory "" (K thy) Toplevel.empty;
    2.17 +    val init = Toplevel.init_theory NONE "" (K thy) Toplevel.empty;
    2.18      val result = fold Toplevel.command (init :: trs) Toplevel.toplevel;
    2.19    in
    2.20      (case (Toplevel.is_theory result, Toplevel.generic_theory_of result) of
     3.1 --- a/src/Pure/Isar/toplevel.ML	Thu Jan 13 17:30:52 2011 +0100
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Jan 13 17:34:45 2011 +0100
     3.3 @@ -45,8 +45,9 @@
     3.4    val set_print: bool -> transition -> transition
     3.5    val print: transition -> transition
     3.6    val no_timing: transition -> transition
     3.7 -  val init_theory: string -> (unit -> theory) -> transition -> transition
     3.8 -  val modify_init: (unit -> theory) -> transition -> transition
     3.9 +  val init_theory: Path.T option -> string -> (Path.T option -> theory) -> transition -> transition
    3.10 +  val modify_master: Path.T option -> transition -> transition
    3.11 +  val modify_init: (Path.T option -> theory) -> transition -> transition
    3.12    val exit: transition -> transition
    3.13    val keep: (state -> unit) -> transition -> transition
    3.14    val keep': (bool -> state -> unit) -> transition -> transition
    3.15 @@ -288,16 +289,16 @@
    3.16  (* primitive transitions *)
    3.17  
    3.18  datatype trans =
    3.19 -  Init of string * (unit -> theory) |    (*theory name, init*)
    3.20 +  Init of Path.T option * string * (Path.T option -> theory) | (*master dir, theory name, init*)
    3.21    Exit |                                 (*formal exit of theory*)
    3.22    Keep of bool -> state -> unit |        (*peek at state*)
    3.23    Transaction of (bool -> node -> node) * (state -> unit);  (*node transaction and presentation*)
    3.24  
    3.25  local
    3.26  
    3.27 -fun apply_tr _ (Init (_, f)) (State (NONE, _)) =
    3.28 +fun apply_tr _ (Init (master, _, f)) (State (NONE, _)) =
    3.29        State (SOME (Theory (Context.Theory
    3.30 -          (Theory.checkpoint (Runtime.controlled_execution f ())), NONE)), NONE)
    3.31 +          (Theory.checkpoint (Runtime.controlled_execution f master)), NONE)), NONE)
    3.32    | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _)), _)) =
    3.33        State (NONE, prev)
    3.34    | apply_tr int (Keep f) state =
    3.35 @@ -344,9 +345,10 @@
    3.36  
    3.37  (* diagnostics *)
    3.38  
    3.39 -fun init_of (Transition {trans = [Init (name, _)], ...}) = SOME name
    3.40 -  | init_of _ = NONE;
    3.41 +fun get_init (Transition {trans = [Init args], ...}) = SOME args
    3.42 +  | get_init _ = NONE;
    3.43  
    3.44 +val init_of = Option.map #2 o get_init;
    3.45  fun print_of (Transition {print, ...}) = print;
    3.46  fun name_of (Transition {name, ...}) = name;
    3.47  fun pos_of (Transition {pos, ...}) = pos;
    3.48 @@ -387,11 +389,16 @@
    3.49  
    3.50  (* basic transitions *)
    3.51  
    3.52 -fun init_theory name f = add_trans (Init (name, f));
    3.53 +fun init_theory master name f = add_trans (Init (master, name, f));
    3.54 +
    3.55 +fun modify_master master tr =
    3.56 +  (case get_init tr of
    3.57 +    SOME (_, name, f) => init_theory master name f (reset_trans tr)
    3.58 +  | NONE => tr);
    3.59  
    3.60  fun modify_init f tr =
    3.61 -  (case init_of tr of
    3.62 -    SOME name => init_theory name f (reset_trans tr)
    3.63 +  (case get_init tr of
    3.64 +    SOME (master, name, _) => init_theory master name f (reset_trans tr)
    3.65    | NONE => tr);
    3.66  
    3.67  val exit = add_trans Exit;
     4.1 --- a/src/Pure/Thy/thy_info.ML	Thu Jan 13 17:30:52 2011 +0100
     4.2 +++ b/src/Pure/Thy/thy_info.ML	Thu Jan 13 17:34:45 2011 +0100
     4.3 @@ -20,7 +20,8 @@
     4.4    val use_thys_wrt: Path.T -> string list -> unit
     4.5    val use_thys: string list -> unit
     4.6    val use_thy: string -> unit
     4.7 -  val toplevel_begin_theory: string -> string list -> (Path.T * bool) list -> theory
     4.8 +  val toplevel_begin_theory: Path.T option -> string ->
     4.9 +    string list -> (Path.T * bool) list -> theory
    4.10    val register_thy: theory -> unit
    4.11    val finish: unit -> unit
    4.12  end;
    4.13 @@ -228,7 +229,7 @@
    4.14      val dir = Path.dir thy_path;
    4.15      val pos = Path.position thy_path;
    4.16      val uses = map (apfst Path.explode) (#3 (Thy_Header.read pos text));
    4.17 -    fun init () =
    4.18 +    fun init _ =
    4.19        Thy_Load.begin_theory dir name parent_thys uses
    4.20        |> Present.begin_theory update_time dir uses;
    4.21  
    4.22 @@ -317,9 +318,9 @@
    4.23  
    4.24  (* toplevel begin theory -- without maintaining database *)
    4.25  
    4.26 -fun toplevel_begin_theory name imports uses =
    4.27 +fun toplevel_begin_theory master name imports uses =
    4.28    let
    4.29 -    val dir = Thy_Load.get_master_path ();
    4.30 +    val dir = (case master of SOME dir => dir | NONE => Thy_Load.get_master_path ());
    4.31      val _ = kill_thy name;
    4.32      val _ = use_thys_wrt dir imports;
    4.33      val parent_thys = map (get_theory o base_name) imports;