Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;

--- a/src/Pure/Isar/isar_syn.ML	Thu Jan 13 17:30:52 2011 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jan 13 17:34:45 2011 +0100
@@ -30,8 +30,9 @@
   Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
     (Thy_Header.args >> (fn (name, imports, uses) =>
       Toplevel.print o
-        Toplevel.init_theory name
-          (fn () => Thy_Info.toplevel_begin_theory name imports (map (apfst Path.explode) uses))));
+        Toplevel.init_theory NONE name
+          (fn master =>
+            Thy_Info.toplevel_begin_theory master name imports (map (apfst Path.explode) uses))));
 
 val _ =
   Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)

--- a/src/Pure/Isar/outer_syntax.ML	Thu Jan 13 17:30:52 2011 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Jan 13 17:34:45 2011 +0100
@@ -31,7 +31,7 @@
   type isar
   val isar: TextIO.instream -> bool -> isar
   val prepare_command: Position.T -> string -> Toplevel.transition
-  val load_thy: string -> (unit -> theory) -> Position.T -> string -> (unit -> unit) * theory
+  val load_thy: string -> (Path.T option -> theory) -> Position.T -> string -> (unit -> unit) * theory
 end;
 
 structure Outer_Syntax: OUTER_SYNTAX =
@@ -204,7 +204,7 @@
 fun process_file path thy =
   let
     val trs = parse (Path.position path) (File.read path);
-    val init = Toplevel.init_theory "" (K thy) Toplevel.empty;
+    val init = Toplevel.init_theory NONE "" (K thy) Toplevel.empty;
     val result = fold Toplevel.command (init :: trs) Toplevel.toplevel;
   in
     (case (Toplevel.is_theory result, Toplevel.generic_theory_of result) of

--- a/src/Pure/Isar/toplevel.ML	Thu Jan 13 17:30:52 2011 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Jan 13 17:34:45 2011 +0100
@@ -45,8 +45,9 @@
   val set_print: bool -> transition -> transition
   val print: transition -> transition
   val no_timing: transition -> transition
-  val init_theory: string -> (unit -> theory) -> transition -> transition
-  val modify_init: (unit -> theory) -> transition -> transition
+  val init_theory: Path.T option -> string -> (Path.T option -> theory) -> transition -> transition
+  val modify_master: Path.T option -> transition -> transition
+  val modify_init: (Path.T option -> theory) -> transition -> transition
   val exit: transition -> transition
   val keep: (state -> unit) -> transition -> transition
   val keep': (bool -> state -> unit) -> transition -> transition
@@ -288,16 +289,16 @@
 (* primitive transitions *)
 
 datatype trans =
-  Init of string * (unit -> theory) |    (*theory name, init*)
+  Init of Path.T option * string * (Path.T option -> theory) | (*master dir, theory name, init*)
   Exit |                                 (*formal exit of theory*)
   Keep of bool -> state -> unit |        (*peek at state*)
   Transaction of (bool -> node -> node) * (state -> unit);  (*node transaction and presentation*)
 
 local
 
-fun apply_tr _ (Init (_, f)) (State (NONE, _)) =
+fun apply_tr _ (Init (master, _, f)) (State (NONE, _)) =
       State (SOME (Theory (Context.Theory
-          (Theory.checkpoint (Runtime.controlled_execution f ())), NONE)), NONE)
+          (Theory.checkpoint (Runtime.controlled_execution f master)), NONE)), NONE)
   | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _)), _)) =
       State (NONE, prev)
   | apply_tr int (Keep f) state =
@@ -344,9 +345,10 @@
 
 (* diagnostics *)
 
-fun init_of (Transition {trans = [Init (name, _)], ...}) = SOME name
-  | init_of _ = NONE;
+fun get_init (Transition {trans = [Init args], ...}) = SOME args
+  | get_init _ = NONE;
 
+val init_of = Option.map #2 o get_init;
 fun print_of (Transition {print, ...}) = print;
 fun name_of (Transition {name, ...}) = name;
 fun pos_of (Transition {pos, ...}) = pos;
@@ -387,11 +389,16 @@
 
 (* basic transitions *)
 
-fun init_theory name f = add_trans (Init (name, f));
+fun init_theory master name f = add_trans (Init (master, name, f));
+
+fun modify_master master tr =
+  (case get_init tr of
+    SOME (_, name, f) => init_theory master name f (reset_trans tr)
+  | NONE => tr);
 
 fun modify_init f tr =
-  (case init_of tr of
-    SOME name => init_theory name f (reset_trans tr)
+  (case get_init tr of
+    SOME (master, name, _) => init_theory master name f (reset_trans tr)
   | NONE => tr);
 
 val exit = add_trans Exit;

--- a/src/Pure/Thy/thy_info.ML	Thu Jan 13 17:30:52 2011 +0100
+++ b/src/Pure/Thy/thy_info.ML	Thu Jan 13 17:34:45 2011 +0100
@@ -20,7 +20,8 @@
   val use_thys_wrt: Path.T -> string list -> unit
   val use_thys: string list -> unit
   val use_thy: string -> unit
-  val toplevel_begin_theory: string -> string list -> (Path.T * bool) list -> theory
+  val toplevel_begin_theory: Path.T option -> string ->
+    string list -> (Path.T * bool) list -> theory
   val register_thy: theory -> unit
   val finish: unit -> unit
 end;
@@ -228,7 +229,7 @@
     val dir = Path.dir thy_path;
     val pos = Path.position thy_path;
     val uses = map (apfst Path.explode) (#3 (Thy_Header.read pos text));
-    fun init () =
+    fun init _ =
       Thy_Load.begin_theory dir name parent_thys uses
       |> Present.begin_theory update_time dir uses;
 
@@ -317,9 +318,9 @@
 
 (* toplevel begin theory -- without maintaining database *)
 
-fun toplevel_begin_theory name imports uses =
+fun toplevel_begin_theory master name imports uses =
   let
-    val dir = Thy_Load.get_master_path ();
+    val dir = (case master of SOME dir => dir | NONE => Thy_Load.get_master_path ());
     val _ = kill_thy name;
     val _ = use_thys_wrt dir imports;
     val parent_thys = map (get_theory o base_name) imports;