src/Pure/General/path.ML
changeset 17827 b32fad049413
parent 15570 8d8c70b41bab
child 19305 5c16895d548b
     1.1 --- a/src/Pure/General/path.ML	Tue Oct 11 14:02:32 2005 +0200
     1.2 +++ b/src/Pure/General/path.ML	Tue Oct 11 14:02:33 2005 +0200
     1.3 @@ -145,17 +145,15 @@
     1.4    | (cs, e) => (Path [Basic (implode (Library.take (length cs - 1, cs)))], implode e)));
     1.5  
     1.6  
     1.7 -(* evaluate variables *)
     1.8 -
     1.9 -fun eval env (Variable s) = rep (env s)
    1.10 -  | eval _ x = [x];
    1.11 +(* expand variables *)
    1.12  
    1.13 -fun evaluate env (Path xs) =
    1.14 -  Path (norm (List.concat (map (eval env) xs)));
    1.15 +fun eval (Variable s) =
    1.16 +    (case getenv s of
    1.17 +      "" => error ("Undefined Isabelle environment variable: " ^ quote s)
    1.18 +    | path => rep (unpack path))
    1.19 +  | eval x = [x];
    1.20  
    1.21 -val expand = evaluate (unpack o getenv);
    1.22 -
    1.23 -val position = Position.line_name 1 o quote o pack o expand;
    1.24 -
    1.25 +val expand = rep #> map eval #> List.concat #> norm #> Path;
    1.26 +val position = expand #> pack #> quote #> Position.line_name 1;
    1.27  
    1.28  end;