moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
authorwenzelm
Tue Jul 17 13:19:21 2007 +0200 (2007-07-17 ago)
changeset 23826463903573934
parent 23825 e0372eba47b7
child 23827 0f0d1cf4992d
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
src/Pure/General/file.ML
src/Pure/ML-Systems/alice.ML
src/Pure/ML-Systems/mosml.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/library.ML
     1.1 --- a/src/Pure/General/file.ML	Tue Jul 17 13:19:20 2007 +0200
     1.2 +++ b/src/Pure/General/file.ML	Tue Jul 17 13:19:21 2007 +0200
     1.3 @@ -52,8 +52,8 @@
     1.4  
     1.5  (* current path *)
     1.6  
     1.7 -val cd = Library.cd o platform_path;
     1.8 -val pwd = explode_platform_path o Library.pwd;
     1.9 +val cd = cd o platform_path;
    1.10 +val pwd = explode_platform_path o pwd;
    1.11  
    1.12  fun norm_absolute p =
    1.13    let
     2.1 --- a/src/Pure/ML-Systems/alice.ML	Tue Jul 17 13:19:20 2007 +0200
     2.2 +++ b/src/Pure/ML-Systems/alice.ML	Tue Jul 17 13:19:21 2007 +0200
     2.3 @@ -2,6 +2,14 @@
     2.4      ID:         $Id$
     2.5  
     2.6  Compatibility file for Alice 1.4.
     2.7 +
     2.8 +NOTE: there is no wrapper script; may run it interactively as follows:
     2.9 +
    2.10 +$ cd Isabelle/src/Pure
    2.11 +$ env ALICE_JIT_MODE=0 alice
    2.12 +- use "ML-Systems/alice.ML";
    2.13 +- use "ROOT.ML";
    2.14 +- Session.finish ();
    2.15  *)
    2.16  
    2.17  fun exit 0 = (OS.Process.exit OS.Process.success): unit
    2.18 @@ -119,6 +127,12 @@
    2.19  
    2.20  (** OS related **)
    2.21  
    2.22 +(* current directory *)
    2.23 +
    2.24 +val cd = OS.FileSys.chDir;
    2.25 +val pwd = OS.FileSys.getDir;
    2.26 +
    2.27 +
    2.28  (* system command execution *)
    2.29  
    2.30  (*execute Unix command which doesn't take any input from stdin and
     3.1 --- a/src/Pure/ML-Systems/mosml.ML	Tue Jul 17 13:19:20 2007 +0200
     3.2 +++ b/src/Pure/ML-Systems/mosml.ML	Tue Jul 17 13:19:21 2007 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  
     3.5  NOTE: saving images does not work; may run it interactively as follows:
     3.6  
     3.7 -$ cd ~~/src/Pure
     3.8 +$ cd Isabelle/src/Pure
     3.9  $ isabelle RAW_ML_SYSTEM
    3.10  > val ml_system = "mosml";
    3.11  > use "ML-Systems/mosml.ML";
    3.12 @@ -164,6 +164,12 @@
    3.13  
    3.14  (** OS related **)
    3.15  
    3.16 +(* current directory *)
    3.17 +
    3.18 +val cd = OS.FileSys.chDir;
    3.19 +val pwd = OS.FileSys.getDir;
    3.20 +
    3.21 +
    3.22  (* system command execution *)
    3.23  
    3.24  (*execute Unix command which doesn't take any input from stdin and
     4.1 --- a/src/Pure/ML-Systems/polyml.ML	Tue Jul 17 13:19:20 2007 +0200
     4.2 +++ b/src/Pure/ML-Systems/polyml.ML	Tue Jul 17 13:19:21 2007 +0200
     4.3 @@ -151,6 +151,12 @@
     4.4  use "ML-Systems/polyml-posix.ML";
     4.5  
     4.6  
     4.7 +(* current directory *)
     4.8 +
     4.9 +val cd = OS.FileSys.chDir;
    4.10 +val pwd = OS.FileSys.getDir;
    4.11 +
    4.12 +
    4.13  (* system command execution *)
    4.14  
    4.15  (*execute Unix command which doesn't take any input from stdin and
     5.1 --- a/src/Pure/ML-Systems/smlnj.ML	Tue Jul 17 13:19:20 2007 +0200
     5.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Tue Jul 17 13:19:21 2007 +0200
     5.3 @@ -216,6 +216,12 @@
     5.4  
     5.5  (** OS related **)
     5.6  
     5.7 +(* current directory *)
     5.8 +
     5.9 +val cd = OS.FileSys.chDir;
    5.10 +val pwd = OS.FileSys.getDir;
    5.11 +
    5.12 +
    5.13  (* system command execution *)
    5.14  
    5.15  (*execute Unix command which doesn't take any input from stdin and
     6.1 --- a/src/Pure/library.ML	Tue Jul 17 13:19:20 2007 +0200
     6.2 +++ b/src/Pure/library.ML	Tue Jul 17 13:19:21 2007 +0200
     6.3 @@ -217,10 +217,6 @@
     6.4    val one_of: 'a list -> 'a
     6.5    val frequency: (int * 'a) list -> 'a
     6.6  
     6.7 -  (*current directory*)
     6.8 -  val cd: string -> unit
     6.9 -  val pwd: unit -> string
    6.10 -
    6.11    (*misc*)
    6.12    val divide_and_conquer: ('a -> 'a list * ('b list -> 'b)) -> 'a -> 'b
    6.13    val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
    6.14 @@ -1018,13 +1014,6 @@
    6.15  
    6.16  
    6.17  
    6.18 -(** current directory **)
    6.19 -
    6.20 -val cd = OS.FileSys.chDir;
    6.21 -val pwd = OS.FileSys.getDir;
    6.22 -
    6.23 -
    6.24 -
    6.25  (** misc **)
    6.26  
    6.27  fun divide_and_conquer decomp x =