# HG changeset patch
# User wenzelm
# Date 1457384001 -3600
# Node ID df62e1ab7d884eb2a7ff0033200673674ef09ea2
# Parent  f1baa15a6a0c1c75f9842e99107505fd12d17a1c
discontinued cd, pwd;

diff -r f1baa15a6a0c -r df62e1ab7d88 NEWS
--- 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 ***
 
diff -r f1baa15a6a0c -r df62e1ab7d88 src/Doc/System/Misc.thy
--- 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>
 
 
diff -r f1baa15a6a0c -r df62e1ab7d88 src/Pure/General/file.ML
--- 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;
 
 
diff -r f1baa15a6a0c -r df62e1ab7d88 src/Pure/ROOT.ML
--- 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;
diff -r f1baa15a6a0c -r df62e1ab7d88 src/Pure/library.ML
--- 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 =