# HG changeset patch
# User wenzelm
# Date 1309435195 -7200
# Node ID 8f777c2e4638eba589e2045ac4749c32d2b530da
# Parent  8c89a1fb30f230079aa584c35f02cb1f96bda164
getenv_strict in ML;
tuned;

diff -r 8c89a1fb30f2 -r 8f777c2e4638 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Thu Jun 30 13:21:41 2011 +0200
+++ b/src/Pure/General/path.ML	Thu Jun 30 13:59:55 2011 +0200
@@ -179,20 +179,11 @@
 
 (* expand variables *)
 
-local
-
-fun eval (Variable s) =
-      (case getenv s of
-        "" => error ("Undefined Isabelle environment variable: " ^ quote s)
-      | path => rep (explode_path path))
+fun eval (Variable s) = rep (explode_path (getenv_strict s))
   | eval x = [x];
 
-in
-
 val expand = rep #> maps eval #> norm #> Path;
 
-end;
-
 
 (* source position *)
 
diff -r 8c89a1fb30f2 -r 8f777c2e4638 src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Thu Jun 30 13:21:41 2011 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Thu Jun 30 13:59:55 2011 +0200
@@ -73,23 +73,6 @@
 
 
 
-(** OS related **)
-
-(* current directory *)
-
-val cd = OS.FileSys.chDir;
-val pwd = OS.FileSys.getDir;
-
-
-(* getenv *)
-
-fun getenv var =
-  (case OS.Process.getEnv var of
-    NONE => ""
-  | SOME txt => txt);
-
-
-
 (** Runtime system **)
 
 val exception_trace = PolyML.exception_trace;
diff -r 8c89a1fb30f2 -r 8f777c2e4638 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Thu Jun 30 13:21:41 2011 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Thu Jun 30 13:59:55 2011 +0200
@@ -159,19 +159,3 @@
 
 use "ML-Systems/unsynchronized.ML";
 
-
-
-(** OS related **)
-
-(* current directory *)
-
-val cd = OS.FileSys.chDir;
-val pwd = OS.FileSys.getDir;
-
-
-(* getenv *)
-
-fun getenv var =
-  (case OS.Process.getEnv var of
-    NONE => ""
-  | SOME txt => txt);
diff -r 8c89a1fb30f2 -r 8f777c2e4638 src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Jun 30 13:21:41 2011 +0200
+++ b/src/Pure/library.ML	Thu Jun 30 13:59:55 2011 +0200
@@ -218,6 +218,10 @@
   val serial: unit -> serial
   val serial_string: unit -> string
   structure Object: sig type T = exn end
+  val cd: string -> unit
+  val pwd: unit -> string
+  val getenv: string -> string
+  val getenv_strict: string -> string
 end;
 
 signature LIBRARY =
@@ -1079,6 +1083,25 @@
   constructors at any time*)
 structure Object = struct type T = exn end;
 
+
+(* current directory *)
+
+val cd = OS.FileSys.chDir;
+val pwd = OS.FileSys.getDir;
+
+
+(* getenv *)
+
+fun getenv x =
+  (case OS.Process.getEnv x of
+    NONE => ""
+  | SOME y => y);
+
+fun getenv_strict x =
+  (case getenv x of
+    "" => error ("Undefined Isabelle environment variable: " ^ quote x)
+  | y => y);
+
 end;
 
 structure Basic_Library: BASIC_LIBRARY = Library;