theory loader: implicit load path is considered legacy;
authorwenzelm
Wed Dec 29 18:18:42 2010 +0100 (2010-12-29)
changeset 4141400b2b6716ed8
parent 41413 64cd30d6b0b8
child 41415 23533273220a
child 41417 211dbd42f95d
theory loader: implicit load path is considered legacy;
NEWS
src/HOL/HOLCF/HOLCF.thy
src/HOL/Plain.thy
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/Thy/thy_load.ML
     1.1 --- a/NEWS	Wed Dec 29 17:34:41 2010 +0100
     1.2 +++ b/NEWS	Wed Dec 29 18:18:42 2010 +0100
     1.3 @@ -84,6 +84,10 @@
     1.4  floating-point notation that coincides with the inner syntax for
     1.5  float_token.
     1.6  
     1.7 +* Theory loader: implicit load path is considered legacy.  Use
     1.8 +explicit file specifications instead, relatively to the directory of
     1.9 +the enclosing theory file.
    1.10 +
    1.11  
    1.12  *** Pure ***
    1.13  
     2.1 --- a/src/HOL/HOLCF/HOLCF.thy	Wed Dec 29 17:34:41 2010 +0100
     2.2 +++ b/src/HOL/HOLCF/HOLCF.thy	Wed Dec 29 18:18:42 2010 +0100
     2.3 @@ -13,7 +13,7 @@
     2.4  
     2.5  default_sort "domain"
     2.6  
     2.7 -ML {* path_add "~~/src/HOL/HOLCF/Library" *}
     2.8 +ML {* Thy_Load.legacy_path_add "~~/src/HOL/HOLCF/Library" *}
     2.9  
    2.10  text {* Legacy theorem names deprecated after Isabelle2009-2: *}
    2.11  
     3.1 --- a/src/HOL/Plain.thy	Wed Dec 29 17:34:41 2010 +0100
     3.2 +++ b/src/HOL/Plain.thy	Wed Dec 29 18:18:42 2010 +0100
     3.3 @@ -9,6 +9,6 @@
     3.4    include @{text Hilbert_Choice}.
     3.5  *}
     3.6  
     3.7 -ML {* path_add "~~/src/HOL/Library" *}
     3.8 +ML {* Thy_Load.legacy_path_add "~~/src/HOL/Library" *}
     3.9  
    3.10  end
     4.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Dec 29 17:34:41 2010 +0100
     4.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Dec 29 18:18:42 2010 +0100
     4.3 @@ -780,8 +780,8 @@
     4.4     in
     4.5         (case (!current_working_dir) of
     4.6              NONE => ()
     4.7 -          | SOME dir => Thy_Load.del_path dir;
     4.8 -        Thy_Load.add_path newdir;
     4.9 +          | SOME dir => Thy_Load.legacy_del_path dir;
    4.10 +        Thy_Load.legacy_add_path newdir;
    4.11          current_working_dir := SOME newdir)
    4.12     end
    4.13  end
     5.1 --- a/src/Pure/Thy/thy_load.ML	Wed Dec 29 17:34:41 2010 +0100
     5.2 +++ b/src/Pure/Thy/thy_load.ML	Wed Dec 29 18:18:42 2010 +0100
     5.3 @@ -5,18 +5,8 @@
     5.4  management.
     5.5  *)
     5.6  
     5.7 -signature BASIC_THY_LOAD =
     5.8 -sig
     5.9 -  val show_path: unit -> string list
    5.10 -  val add_path: string -> unit
    5.11 -  val path_add: string -> unit
    5.12 -  val del_path: string -> unit
    5.13 -  val reset_path: unit -> unit
    5.14 -end;
    5.15 -
    5.16  signature THY_LOAD =
    5.17  sig
    5.18 -  include BASIC_THY_LOAD
    5.19    eqtype file_ident
    5.20    val pretty_file_ident: file_ident -> Pretty.T
    5.21    val file_ident: Path.T -> file_ident option
    5.22 @@ -24,6 +14,11 @@
    5.23    val get_master_path: unit -> Path.T
    5.24    val master_directory: theory -> Path.T
    5.25    val provide: Path.T * (Path.T * file_ident) -> theory -> theory
    5.26 +  val legacy_show_path: unit -> string list
    5.27 +  val legacy_add_path: string -> unit
    5.28 +  val legacy_path_add: string -> unit
    5.29 +  val legacy_del_path: string -> unit
    5.30 +  val legacy_reset_path: unit -> unit
    5.31    val check_file: Path.T list -> Path.T -> Path.T * file_ident
    5.32    val check_thy: Path.T -> string -> Path.T * file_ident
    5.33    val deps_thy: Path.T -> string ->
    5.34 @@ -131,18 +126,18 @@
    5.35    val master_path = Unsynchronized.ref Path.current;
    5.36  in
    5.37  
    5.38 -fun show_path () = map Path.implode (Synchronized.value load_path);
    5.39 +fun legacy_show_path () = map Path.implode (Synchronized.value load_path);
    5.40  
    5.41 -fun del_path s = Synchronized.change load_path (remove (op =) (Path.explode s));
    5.42 +fun legacy_del_path s = Synchronized.change load_path (remove (op =) (Path.explode s));
    5.43  
    5.44 -fun add_path s = Synchronized.change load_path (update (op =) (Path.explode s));
    5.45 +fun legacy_add_path s = Synchronized.change load_path (update (op =) (Path.explode s));
    5.46  
    5.47 -fun path_add s =
    5.48 +fun legacy_path_add s =
    5.49    Synchronized.change load_path (fn path =>
    5.50      let val p = Path.explode s
    5.51      in remove (op =) p path @ [p] end);
    5.52  
    5.53 -fun reset_path () = Synchronized.change load_path (K [Path.current]);
    5.54 +fun legacy_reset_path () = Synchronized.change load_path (K [Path.current]);
    5.55  
    5.56  fun search_path dir path =
    5.57    distinct (op =)
    5.58 @@ -265,5 +260,3 @@
    5.59  
    5.60  end;
    5.61  
    5.62 -structure Basic_Thy_Load: BASIC_THY_LOAD = Thy_Load;
    5.63 -open Basic_Thy_Load;