# HG changeset patch # User wenzelm # Date 1184671161 -7200 # Node ID 4639035739343f9be9a899ae57a64c86eada7803 # Parent e0372eba47b7b1ee77f199141cb5ae29cb20e5f9 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice); diff -r e0372eba47b7 -r 463903573934 src/Pure/General/file.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 diff -r e0372eba47b7 -r 463903573934 src/Pure/ML-Systems/alice.ML --- 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 diff -r e0372eba47b7 -r 463903573934 src/Pure/ML-Systems/mosml.ML --- 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 diff -r e0372eba47b7 -r 463903573934 src/Pure/ML-Systems/polyml.ML --- 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 diff -r e0372eba47b7 -r 463903573934 src/Pure/ML-Systems/smlnj.ML --- 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 diff -r e0372eba47b7 -r 463903573934 src/Pure/library.ML --- 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 =