# HG changeset patch
# User wenzelm
# Date 1129032153 -7200
# Node ID b32fad049413d8815b60a33cb8d85eb5d49136a9
# Parent  afa2696eacce989c1994a98b8c5169e31d8d3319
expand: error on undefined/empty env variable;
tuned;

diff -r afa2696eacce -r b32fad049413 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Tue Oct 11 14:02:32 2005 +0200
+++ b/src/Pure/General/path.ML	Tue Oct 11 14:02:33 2005 +0200
@@ -145,17 +145,15 @@
   | (cs, e) => (Path [Basic (implode (Library.take (length cs - 1, cs)))], implode e)));
 
 
-(* evaluate variables *)
-
-fun eval env (Variable s) = rep (env s)
-  | eval _ x = [x];
+(* expand variables *)
 
-fun evaluate env (Path xs) =
-  Path (norm (List.concat (map (eval env) xs)));
+fun eval (Variable s) =
+    (case getenv s of
+      "" => error ("Undefined Isabelle environment variable: " ^ quote s)
+    | path => rep (unpack path))
+  | eval x = [x];
 
-val expand = evaluate (unpack o getenv);
-
-val position = Position.line_name 1 o quote o pack o expand;
-
+val expand = rep #> map eval #> List.concat #> norm #> Path;
+val position = expand #> pack #> quote #> Position.line_name 1;
 
 end;