--- a/NEWS Thu Mar 03 15:56:17 2011 +0100
+++ b/NEWS Thu Mar 03 18:10:28 2011 +0100
@@ -16,6 +16,11 @@
* Discontinued old lib/scripts/polyml-platform, which has been
obsolete since Isabelle2009-2.
+* Theory loader: source files are exclusively located via the master
+directory of each theory node (where the .thy file itself resides).
+The global load path (such as src/HOL/Library) is has been
+discontinued. INCOMPATIBILITY.
+
*** HOL ***
--- a/src/HOL/HOLCF/HOLCF.thy Thu Mar 03 15:56:17 2011 +0100
+++ b/src/HOL/HOLCF/HOLCF.thy Thu Mar 03 18:10:28 2011 +0100
@@ -13,8 +13,6 @@
default_sort "domain"
-ML {* Thy_Load.legacy_path_add "~~/src/HOL/HOLCF/Library" *}
-
text {* Legacy theorem names deprecated after Isabelle2009-2: *}
lemmas expand_fun_below = fun_below_iff
--- a/src/HOL/Plain.thy Thu Mar 03 15:56:17 2011 +0100
+++ b/src/HOL/Plain.thy Thu Mar 03 18:10:28 2011 +0100
@@ -9,6 +9,4 @@
include @{text Hilbert_Choice}.
*}
-ML {* Thy_Load.legacy_path_add "~~/src/HOL/Library" *}
-
end
--- a/src/Pure/ProofGeneral/pgip_isabelle.ML Thu Mar 03 15:56:17 2011 +0100
+++ b/src/Pure/ProofGeneral/pgip_isabelle.ML Thu Mar 03 18:10:28 2011 +0100
@@ -80,7 +80,7 @@
NONE => (NONE, NONE)
| SOME fname =>
let val path = Path.explode fname in
- if can (Thy_Load.check_file [Path.current]) path
+ if can (Thy_Load.check_file Path.current) path
then (SOME (PgipTypes.pgipurl_of_path path), NONE)
else (NONE, SOME fname)
end);
--- a/src/Pure/Thy/present.ML Thu Mar 03 15:56:17 2011 +0100
+++ b/src/Pure/Thy/present.ML Thu Mar 03 18:10:28 2011 +0100
@@ -462,7 +462,7 @@
val files_html = files |> map (fn (raw_path, loadit) =>
let
- val path = #1 (Thy_Load.check_file [dir] raw_path);
+ val path = #1 (Thy_Load.check_file dir raw_path);
val base = Path.base path;
val base_html = html_ext base;
val _ = add_file (Path.append html_prefix base_html,
--- a/src/Pure/Thy/thy_load.ML Thu Mar 03 15:56:17 2011 +0100
+++ b/src/Pure/Thy/thy_load.ML Thu Mar 03 18:10:28 2011 +0100
@@ -15,12 +15,7 @@
val master_directory: theory -> Path.T
val imports_of: theory -> string list
val provide: Path.T * (Path.T * file_ident) -> theory -> theory
- val legacy_show_path: unit -> string list
- val legacy_add_path: string -> unit
- val legacy_path_add: string -> unit
- val legacy_del_path: string -> unit
- val legacy_reset_path: unit -> unit
- val check_file: Path.T list -> Path.T -> Path.T * file_ident
+ val check_file: Path.T -> Path.T -> Path.T * file_ident
val check_thy: Path.T -> string -> Path.T * file_ident
val deps_thy: Path.T -> string ->
{master: Path.T * file_ident, text: string, imports: string list, uses: Path.T list}
@@ -122,30 +117,12 @@
else (master_dir, imports, required, (src_path, path_id) :: provided));
-(* maintain default paths *)
+(* stateful master path *)
local
- val load_path = Synchronized.var "load_path" [Path.current];
val master_path = Unsynchronized.ref Path.current;
in
-fun legacy_show_path () = map Path.implode (Synchronized.value load_path);
-
-fun legacy_del_path s = Synchronized.change load_path (remove (op =) (Path.explode s));
-
-fun legacy_add_path s = Synchronized.change load_path (update (op =) (Path.explode s));
-
-fun legacy_path_add s =
- Synchronized.change load_path (fn path =>
- let val p = Path.explode s
- in remove (op =) p path @ [p] end);
-
-fun legacy_reset_path () = Synchronized.change load_path (K [Path.current]);
-
-fun search_path dir path =
- distinct (op =)
- (dir :: (if Path.is_basic path then (Synchronized.value load_path) else [Path.current]));
-
fun set_master_path path = master_path := path;
fun get_master_path () = ! master_path;
@@ -154,36 +131,25 @@
(* check files *)
-fun get_file dirs src_path =
+fun get_file dir src_path =
let
val path = Path.expand src_path;
val _ = Path.is_current path andalso error "Bad file specification";
+ val full_path = File.full_path (Path.append dir path);
in
- dirs |> get_first (fn dir =>
- let val full_path = File.full_path (Path.append dir path) in
- (case file_ident full_path of
- NONE => NONE
- | SOME id => SOME (dir, (full_path, id)))
- end)
+ (case file_ident full_path of
+ NONE => NONE
+ | SOME id => SOME (full_path, id))
end;
-fun check_file dirs file =
- (case get_file dirs file of
- SOME (_, path_id) =>
- (if is_some (get_file [hd dirs] file) then ()
- else
- legacy_feature ("File " ^ quote (Path.implode file) ^
- " located via secondary search path: " ^
- quote (Path.implode (#1 (the (get_file (tl dirs) file)))));
- path_id)
+fun check_file dir file =
+ (case get_file dir file of
+ SOME path_id => path_id
| NONE => error ("Could not find file " ^ quote (Path.implode file) ^
- "\nin " ^ commas_quote (map Path.implode dirs)));
+ "\nin " ^ quote (Path.implode dir)));
-fun check_thy master_dir name =
- let
- val thy_file = Thy_Header.thy_path name;
- val dirs = search_path master_dir thy_file;
- in check_file dirs thy_file end;
+fun check_thy dir name =
+ check_file dir (Thy_Header.thy_path name);
(* theory deps *)
@@ -221,9 +187,9 @@
let
val {master_dir, provided, ...} = Files.get thy;
fun current (src_path, (_, id)) =
- (case get_file [master_dir] src_path of
+ (case get_file master_dir src_path of
NONE => false
- | SOME (_, (_, id')) => id = id');
+ | SOME (_, id') => id = id');
in can check_loaded thy andalso forall current provided end;
val _ = Context.>> (Context.map_theory (Theory.at_end (fn thy => (check_loaded thy; NONE))));
@@ -232,15 +198,15 @@
(* provide files *)
fun provide_file src_path thy =
- provide (src_path, check_file [master_directory thy] src_path) thy;
+ provide (src_path, check_file (master_directory thy) src_path) thy;
fun use_ml src_path =
if is_none (Context.thread_data ()) then
- ML_Context.eval_file (#1 (check_file [Path.current] src_path))
+ ML_Context.eval_file (#1 (check_file Path.current src_path))
else
let
val thy = ML_Context.the_global_context ();
- val (path, id) = check_file [master_directory thy] src_path;
+ val (path, id) = check_file (master_directory thy) src_path;
val _ = ML_Context.eval_file path;
val _ = Context.>> Local_Theory.propagate_ml_env;