moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
authorwenzelm
Tue, 17 Jul 2007 13:19:21 +0200
changeset 23826 463903573934
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
--- a/src/Pure/General/file.ML	Tue Jul 17 13:19:20 2007 +0200
+++ b/src/Pure/General/file.ML	Tue Jul 17 13:19:21 2007 +0200
@@ -52,8 +52,8 @@
 
 (* current path *)
 
-val cd = Library.cd o platform_path;
-val pwd = explode_platform_path o Library.pwd;
+val cd = cd o platform_path;
+val pwd = explode_platform_path o pwd;
 
 fun norm_absolute p =
   let
--- a/src/Pure/ML-Systems/alice.ML	Tue Jul 17 13:19:20 2007 +0200
+++ b/src/Pure/ML-Systems/alice.ML	Tue Jul 17 13:19:21 2007 +0200
@@ -2,6 +2,14 @@
     ID:         $Id$
 
 Compatibility file for Alice 1.4.
+
+NOTE: there is no wrapper script; may run it interactively as follows:
+
+$ cd Isabelle/src/Pure
+$ env ALICE_JIT_MODE=0 alice
+- use "ML-Systems/alice.ML";
+- use "ROOT.ML";
+- Session.finish ();
 *)
 
 fun exit 0 = (OS.Process.exit OS.Process.success): unit
@@ -119,6 +127,12 @@
 
 (** OS related **)
 
+(* current directory *)
+
+val cd = OS.FileSys.chDir;
+val pwd = OS.FileSys.getDir;
+
+
 (* system command execution *)
 
 (*execute Unix command which doesn't take any input from stdin and
--- a/src/Pure/ML-Systems/mosml.ML	Tue Jul 17 13:19:20 2007 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Tue Jul 17 13:19:21 2007 +0200
@@ -7,7 +7,7 @@
 
 NOTE: saving images does not work; may run it interactively as follows:
 
-$ cd ~~/src/Pure
+$ cd Isabelle/src/Pure
 $ isabelle RAW_ML_SYSTEM
 > val ml_system = "mosml";
 > use "ML-Systems/mosml.ML";
@@ -164,6 +164,12 @@
 
 (** OS related **)
 
+(* current directory *)
+
+val cd = OS.FileSys.chDir;
+val pwd = OS.FileSys.getDir;
+
+
 (* system command execution *)
 
 (*execute Unix command which doesn't take any input from stdin and
--- a/src/Pure/ML-Systems/polyml.ML	Tue Jul 17 13:19:20 2007 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Tue Jul 17 13:19:21 2007 +0200
@@ -151,6 +151,12 @@
 use "ML-Systems/polyml-posix.ML";
 
 
+(* current directory *)
+
+val cd = OS.FileSys.chDir;
+val pwd = OS.FileSys.getDir;
+
+
 (* system command execution *)
 
 (*execute Unix command which doesn't take any input from stdin and
--- a/src/Pure/ML-Systems/smlnj.ML	Tue Jul 17 13:19:20 2007 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Tue Jul 17 13:19:21 2007 +0200
@@ -216,6 +216,12 @@
 
 (** OS related **)
 
+(* current directory *)
+
+val cd = OS.FileSys.chDir;
+val pwd = OS.FileSys.getDir;
+
+
 (* system command execution *)
 
 (*execute Unix command which doesn't take any input from stdin and
--- a/src/Pure/library.ML	Tue Jul 17 13:19:20 2007 +0200
+++ b/src/Pure/library.ML	Tue Jul 17 13:19:21 2007 +0200
@@ -217,10 +217,6 @@
   val one_of: 'a list -> 'a
   val frequency: (int * 'a) list -> 'a
 
-  (*current directory*)
-  val cd: string -> unit
-  val pwd: unit -> string
-
   (*misc*)
   val divide_and_conquer: ('a -> 'a list * ('b list -> 'b)) -> 'a -> 'b
   val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
@@ -1018,13 +1014,6 @@
 
 
 
-(** current directory **)
-
-val cd = OS.FileSys.chDir;
-val pwd = OS.FileSys.getDir;
-
-
-
 (** misc **)
 
 fun divide_and_conquer decomp x =