# HG changeset patch
# User wenzelm
# Date 1299172228 -3600
# Node ID aa8dce9ab8a9b6ae5ac30b038551a81c5eb11c41
# Parent  1e081bfb2eaf202b86d6cbc6e995c28a87f01250
discontinued legacy load path;

diff -r 1e081bfb2eaf -r aa8dce9ab8a9 NEWS
--- 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 ***
 
diff -r 1e081bfb2eaf -r aa8dce9ab8a9 src/HOL/HOLCF/HOLCF.thy
--- 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
diff -r 1e081bfb2eaf -r aa8dce9ab8a9 src/HOL/Plain.thy
--- 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
diff -r 1e081bfb2eaf -r aa8dce9ab8a9 src/Pure/ProofGeneral/pgip_isabelle.ML
--- 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);
diff -r 1e081bfb2eaf -r aa8dce9ab8a9 src/Pure/Thy/present.ML
--- 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,
diff -r 1e081bfb2eaf -r aa8dce9ab8a9 src/Pure/Thy/thy_load.ML
--- 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;