# HG changeset patch # User wenzelm # Date 1294936485 -3600 # Node ID 47fef6afe756ce8e041d315c6f94fcfd6d7727ab # Parent 0112f14d75ec2a89bdd49ccaf0ec59c6b2aae8f2 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path; diff -r 0112f14d75ec -r 47fef6afe756 src/Pure/Isar/isar_syn.ML --- 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) diff -r 0112f14d75ec -r 47fef6afe756 src/Pure/Isar/outer_syntax.ML --- 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 diff -r 0112f14d75ec -r 47fef6afe756 src/Pure/Isar/toplevel.ML --- 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; diff -r 0112f14d75ec -r 47fef6afe756 src/Pure/Thy/thy_info.ML --- 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;