theory loader: implicit load path is considered legacy;

--- a/NEWS	Wed Dec 29 17:34:41 2010 +0100
+++ b/NEWS	Wed Dec 29 18:18:42 2010 +0100
@@ -84,6 +84,10 @@
 floating-point notation that coincides with the inner syntax for
 float_token.
 
+* Theory loader: implicit load path is considered legacy.  Use
+explicit file specifications instead, relatively to the directory of
+the enclosing theory file.
+
 
 *** Pure ***
 

--- a/src/HOL/HOLCF/HOLCF.thy	Wed Dec 29 17:34:41 2010 +0100
+++ b/src/HOL/HOLCF/HOLCF.thy	Wed Dec 29 18:18:42 2010 +0100
@@ -13,7 +13,7 @@
 
 default_sort "domain"
 
-ML {* path_add "~~/src/HOL/HOLCF/Library" *}
+ML {* Thy_Load.legacy_path_add "~~/src/HOL/HOLCF/Library" *}
 
 text {* Legacy theorem names deprecated after Isabelle2009-2: *}
 

--- a/src/HOL/Plain.thy	Wed Dec 29 17:34:41 2010 +0100
+++ b/src/HOL/Plain.thy	Wed Dec 29 18:18:42 2010 +0100
@@ -9,6 +9,6 @@
   include @{text Hilbert_Choice}.
 *}
 
-ML {* path_add "~~/src/HOL/Library" *}
+ML {* Thy_Load.legacy_path_add "~~/src/HOL/Library" *}
 
 end

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Dec 29 17:34:41 2010 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Dec 29 18:18:42 2010 +0100
@@ -780,8 +780,8 @@
    in
        (case (!current_working_dir) of
             NONE => ()
-          | SOME dir => Thy_Load.del_path dir;
-        Thy_Load.add_path newdir;
+          | SOME dir => Thy_Load.legacy_del_path dir;
+        Thy_Load.legacy_add_path newdir;
         current_working_dir := SOME newdir)
    end
 end

--- a/src/Pure/Thy/thy_load.ML	Wed Dec 29 17:34:41 2010 +0100
+++ b/src/Pure/Thy/thy_load.ML	Wed Dec 29 18:18:42 2010 +0100
@@ -5,18 +5,8 @@
 management.
 *)
 
-signature BASIC_THY_LOAD =
-sig
-  val show_path: unit -> string list
-  val add_path: string -> unit
-  val path_add: string -> unit
-  val del_path: string -> unit
-  val reset_path: unit -> unit
-end;
-
 signature THY_LOAD =
 sig
-  include BASIC_THY_LOAD
   eqtype file_ident
   val pretty_file_ident: file_ident -> Pretty.T
   val file_ident: Path.T -> file_ident option
@@ -24,6 +14,11 @@
   val get_master_path: unit -> Path.T
   val master_directory: theory -> Path.T
   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_thy: Path.T -> string -> Path.T * file_ident
   val deps_thy: Path.T -> string ->
@@ -131,18 +126,18 @@
   val master_path = Unsynchronized.ref Path.current;
 in
 
-fun show_path () = map Path.implode (Synchronized.value load_path);
+fun legacy_show_path () = map Path.implode (Synchronized.value load_path);
 
-fun del_path s = Synchronized.change load_path (remove (op =) (Path.explode s));
+fun legacy_del_path s = Synchronized.change load_path (remove (op =) (Path.explode s));
 
-fun add_path s = Synchronized.change load_path (update (op =) (Path.explode s));
+fun legacy_add_path s = Synchronized.change load_path (update (op =) (Path.explode s));
 
-fun path_add 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 reset_path () = Synchronized.change load_path (K [Path.current]);
+fun legacy_reset_path () = Synchronized.change load_path (K [Path.current]);
 
 fun search_path dir path =
   distinct (op =)
@@ -265,5 +260,3 @@
 
 end;
 
-structure Basic_Thy_Load: BASIC_THY_LOAD = Thy_Load;
-open Basic_Thy_Load;