tuned;
authorwenzelm
Sun Mar 20 13:49:21 2011 +0100 (2011-03-20)
changeset 42002ac7097bd8611
parent 42001 614ff13dc5d2
child 42003 6e45dc518ebb
tuned;
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/Pure/Thy/thy_load.ML	Sat Mar 19 14:03:13 2011 +0100
     1.2 +++ b/src/Pure/Thy/thy_load.ML	Sun Mar 20 13:49:21 2011 +0100
     1.3 @@ -1,14 +1,11 @@
     1.4  (*  Title:      Pure/Thy/thy_load.ML
     1.5 -    Author:     Markus Wenzel, TU Muenchen
     1.6 +    Author:     Makarius
     1.7  
     1.8 -Loading files that contribute to a theory, including global load path
     1.9 -management.
    1.10 +Loading files that contribute to a theory.  Global master path.
    1.11  *)
    1.12  
    1.13  signature THY_LOAD =
    1.14  sig
    1.15 -  val set_master_path: Path.T -> unit
    1.16 -  val get_master_path: unit -> Path.T
    1.17    val master_directory: theory -> Path.T
    1.18    val imports_of: theory -> string list
    1.19    val provide: Path.T * (Path.T * SHA1.digest) -> theory -> theory
    1.20 @@ -22,6 +19,8 @@
    1.21    val use_ml: Path.T -> unit
    1.22    val exec_ml: Path.T -> generic_theory -> generic_theory
    1.23    val begin_theory: Path.T -> string -> string list -> theory list -> (Path.T * bool) list -> theory
    1.24 +  val set_master_path: Path.T -> unit
    1.25 +  val get_master_path: unit -> Path.T
    1.26  end;
    1.27  
    1.28  structure Thy_Load: THY_LOAD =
    1.29 @@ -69,18 +68,6 @@
    1.30      else (master_dir, imports, required, (src_path, path_id) :: provided));
    1.31  
    1.32  
    1.33 -(* stateful master path *)
    1.34 -
    1.35 -local
    1.36 -  val master_path = Unsynchronized.ref Path.current;
    1.37 -in
    1.38 -
    1.39 -fun set_master_path path = master_path := path;
    1.40 -fun get_master_path () = ! master_path;
    1.41 -
    1.42 -end;
    1.43 -
    1.44 -
    1.45  (* check files *)
    1.46  
    1.47  fun get_file dir src_path =
    1.48 @@ -178,5 +165,16 @@
    1.49    |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses
    1.50    |> Theory.checkpoint;
    1.51  
    1.52 +
    1.53 +(* global master path *)
    1.54 +
    1.55 +local
    1.56 +  val master_path = Unsynchronized.ref Path.current;
    1.57 +in
    1.58 +
    1.59 +fun set_master_path path = master_path := path;
    1.60 +fun get_master_path () = ! master_path;
    1.61 +
    1.62  end;
    1.63  
    1.64 +end;