discontinued cd, pwd;
authorwenzelm
Mon Mar 07 21:53:21 2016 +0100 (2016-03-07)
changeset 62551df62e1ab7d88
parent 62550 f1baa15a6a0c
child 62552 53603d1aad5f
discontinued cd, pwd;
NEWS
src/Doc/System/Misc.thy
src/Pure/General/file.ML
src/Pure/ROOT.ML
src/Pure/library.ML
     1.1 --- a/NEWS	Mon Mar 07 21:33:41 2016 +0100
     1.2 +++ b/NEWS	Mon Mar 07 21:53:21 2016 +0100
     1.3 @@ -210,6 +210,11 @@
     1.4  replaced by structure Timeout, with slightly different signature.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Discontinued cd and pwd operations, which are not well-defined in a
     1.8 +multi-threaded environment. Note that files are usually located
     1.9 +relatively to the master directory of a theory (see also
    1.10 +File.full_path). Potential INCOMPATIBILITY.
    1.11 +
    1.12  
    1.13  *** System ***
    1.14  
     2.1 --- a/src/Doc/System/Misc.thy	Mon Mar 07 21:33:41 2016 +0100
     2.2 +++ b/src/Doc/System/Misc.thy	Mon Mar 07 21:53:21 2016 +0100
     2.3 @@ -94,8 +94,7 @@
     2.4  
     2.5    Interaction works via the raw ML toplevel loop: this is neither
     2.6    Isabelle/Isar nor Isabelle/ML within the usual formal context. Some useful
     2.7 -  ML commands at this stage are @{ML cd}, @{ML pwd}, @{ML use}, @{ML use_thy},
     2.8 -  @{ML use_thys}.
     2.9 +  ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML use_thys}.
    2.10  \<close>
    2.11  
    2.12  
     3.1 --- a/src/Pure/General/file.ML	Mon Mar 07 21:33:41 2016 +0100
     3.2 +++ b/src/Pure/General/file.ML	Mon Mar 07 21:53:21 2016 +0100
     3.3 @@ -11,8 +11,6 @@
     3.4    val bash_string: string -> string
     3.5    val bash_args: string list -> string
     3.6    val bash_path: Path.T -> string
     3.7 -  val cd: Path.T -> unit
     3.8 -  val pwd: unit -> Path.T
     3.9    val full_path: Path.T -> Path.T -> Path.T
    3.10    val tmp_path: Path.T -> Path.T
    3.11    val exists: Path.T -> bool
    3.12 @@ -69,12 +67,6 @@
    3.13  val bash_path = bash_string o standard_path;
    3.14  
    3.15  
    3.16 -(* current working directory *)
    3.17 -
    3.18 -val cd = cd o standard_path;
    3.19 -val pwd = Path.explode o pwd;
    3.20 -
    3.21 -
    3.22  (* full_path *)
    3.23  
    3.24  fun full_path dir path =
    3.25 @@ -84,7 +76,7 @@
    3.26      val path'' = Path.append dir path';
    3.27    in
    3.28      if Path.is_absolute path'' then path''
    3.29 -    else Path.append (pwd ()) path''
    3.30 +    else Path.append (Path.explode (ML_System.standard_path (OS.FileSys.getDir ()))) path''
    3.31    end;
    3.32  
    3.33  
     4.1 --- a/src/Pure/ROOT.ML	Mon Mar 07 21:33:41 2016 +0100
     4.2 +++ b/src/Pure/ROOT.ML	Mon Mar 07 21:53:21 2016 +0100
     4.3 @@ -429,6 +429,4 @@
     4.4    Runtime.toplevel_program (fn () => Thy_Info.use_thys (map (rpair Position.none) args));
     4.5  val use_thy = use_thys o single;
     4.6  
     4.7 -val cd = File.cd o Path.explode;
     4.8 -
     4.9  Proofterm.proofs := 0;
     5.1 --- a/src/Pure/library.ML	Mon Mar 07 21:33:41 2016 +0100
     5.2 +++ b/src/Pure/library.ML	Mon Mar 07 21:53:21 2016 +0100
     5.3 @@ -206,8 +206,6 @@
     5.4    eqtype stamp
     5.5    val stamp: unit -> stamp
     5.6    structure Any: sig type T = exn end
     5.7 -  val cd: string -> unit
     5.8 -  val pwd: unit -> string
     5.9    val getenv: string -> string
    5.10    val getenv_strict: string -> string
    5.11  end;
    5.12 @@ -1014,12 +1012,6 @@
    5.13  structure Any = struct type T = exn end;
    5.14  
    5.15  
    5.16 -(* current directory *)
    5.17 -
    5.18 -val cd = OS.FileSys.chDir o ML_System.platform_path;
    5.19 -val pwd = ML_System.standard_path o OS.FileSys.getDir;
    5.20 -
    5.21 -
    5.22  (* getenv *)
    5.23  
    5.24  fun getenv x =