# HG changeset patch # User wenzelm # Date 1300625361 -3600 # Node ID ac7097bd861118217d043f1c52b452b3f01a764e # Parent 614ff13dc5d29ec345c455ddeb6fb31b94051829 tuned; diff -r 614ff13dc5d2 -r ac7097bd8611 src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Sat Mar 19 14:03:13 2011 +0100 +++ b/src/Pure/Thy/thy_load.ML Sun Mar 20 13:49:21 2011 +0100 @@ -1,14 +1,11 @@ (* Title: Pure/Thy/thy_load.ML - Author: Markus Wenzel, TU Muenchen + Author: Makarius -Loading files that contribute to a theory, including global load path -management. +Loading files that contribute to a theory. Global master path. *) signature THY_LOAD = sig - val set_master_path: Path.T -> unit - val get_master_path: unit -> Path.T val master_directory: theory -> Path.T val imports_of: theory -> string list val provide: Path.T * (Path.T * SHA1.digest) -> theory -> theory @@ -22,6 +19,8 @@ val use_ml: Path.T -> unit val exec_ml: Path.T -> generic_theory -> generic_theory val begin_theory: Path.T -> string -> string list -> theory list -> (Path.T * bool) list -> theory + val set_master_path: Path.T -> unit + val get_master_path: unit -> Path.T end; structure Thy_Load: THY_LOAD = @@ -69,18 +68,6 @@ else (master_dir, imports, required, (src_path, path_id) :: provided)); -(* stateful master path *) - -local - val master_path = Unsynchronized.ref Path.current; -in - -fun set_master_path path = master_path := path; -fun get_master_path () = ! master_path; - -end; - - (* check files *) fun get_file dir src_path = @@ -178,5 +165,16 @@ |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses |> Theory.checkpoint; + +(* global master path *) + +local + val master_path = Unsynchronized.ref Path.current; +in + +fun set_master_path path = master_path := path; +fun get_master_path () = ! master_path; + end; +end;