--- a/NEWS Mon Mar 07 21:33:41 2016 +0100
+++ b/NEWS Mon Mar 07 21:53:21 2016 +0100
@@ -210,6 +210,11 @@
replaced by structure Timeout, with slightly different signature.
INCOMPATIBILITY.
+* Discontinued cd and pwd operations, which are not well-defined in a
+multi-threaded environment. Note that files are usually located
+relatively to the master directory of a theory (see also
+File.full_path). Potential INCOMPATIBILITY.
+
*** System ***
--- a/src/Doc/System/Misc.thy Mon Mar 07 21:33:41 2016 +0100
+++ b/src/Doc/System/Misc.thy Mon Mar 07 21:53:21 2016 +0100
@@ -94,8 +94,7 @@
Interaction works via the raw ML toplevel loop: this is neither
Isabelle/Isar nor Isabelle/ML within the usual formal context. Some useful
- ML commands at this stage are @{ML cd}, @{ML pwd}, @{ML use}, @{ML use_thy},
- @{ML use_thys}.
+ ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML use_thys}.
\<close>
--- a/src/Pure/General/file.ML Mon Mar 07 21:33:41 2016 +0100
+++ b/src/Pure/General/file.ML Mon Mar 07 21:53:21 2016 +0100
@@ -11,8 +11,6 @@
val bash_string: string -> string
val bash_args: string list -> string
val bash_path: Path.T -> string
- val cd: Path.T -> unit
- val pwd: unit -> Path.T
val full_path: Path.T -> Path.T -> Path.T
val tmp_path: Path.T -> Path.T
val exists: Path.T -> bool
@@ -69,12 +67,6 @@
val bash_path = bash_string o standard_path;
-(* current working directory *)
-
-val cd = cd o standard_path;
-val pwd = Path.explode o pwd;
-
-
(* full_path *)
fun full_path dir path =
@@ -84,7 +76,7 @@
val path'' = Path.append dir path';
in
if Path.is_absolute path'' then path''
- else Path.append (pwd ()) path''
+ else Path.append (Path.explode (ML_System.standard_path (OS.FileSys.getDir ()))) path''
end;
--- a/src/Pure/ROOT.ML Mon Mar 07 21:33:41 2016 +0100
+++ b/src/Pure/ROOT.ML Mon Mar 07 21:53:21 2016 +0100
@@ -429,6 +429,4 @@
Runtime.toplevel_program (fn () => Thy_Info.use_thys (map (rpair Position.none) args));
val use_thy = use_thys o single;
-val cd = File.cd o Path.explode;
-
Proofterm.proofs := 0;
--- a/src/Pure/library.ML Mon Mar 07 21:33:41 2016 +0100
+++ b/src/Pure/library.ML Mon Mar 07 21:53:21 2016 +0100
@@ -206,8 +206,6 @@
eqtype stamp
val stamp: unit -> stamp
structure Any: sig type T = exn end
- val cd: string -> unit
- val pwd: unit -> string
val getenv: string -> string
val getenv_strict: string -> string
end;
@@ -1014,12 +1012,6 @@
structure Any = struct type T = exn end;
-(* current directory *)
-
-val cd = OS.FileSys.chDir o ML_System.platform_path;
-val pwd = ML_System.standard_path o OS.FileSys.getDir;
-
-
(* getenv *)
fun getenv x =