src/Pure/General/path.ML
changeset 6223 e8807883e3e3
parent 6187 c6c4626ef693
child 6270 c905fe5994a2
     1.1 --- a/src/Pure/General/path.ML	Thu Feb 04 18:12:26 1999 +0100
     1.2 +++ b/src/Pure/General/path.ML	Thu Feb 04 18:13:10 1999 +0100
     1.3 @@ -33,14 +33,17 @@
     1.4  
     1.5  datatype elem = Root | Parent | Basic of string | Variable of string;
     1.6  
     1.7 -fun no_meta_chars chs =
     1.8 -  (case ["/", "\\", "$", "~"] inter_string chs of
     1.9 -    [] => chs
    1.10 -  | bads => error ("Illegal character(s) " ^ commas_quote bads ^
    1.11 -      " in path element specification: " ^ quote (implode chs)));
    1.12 +fun err_elem msg chs = error (msg ^ " path element specification: " ^ quote (implode chs));
    1.13  
    1.14 -val basic_elem = Basic o implode o no_meta_chars;
    1.15 -val variable_elem = Variable o implode o no_meta_chars;
    1.16 +fun check_elem (chs as ["~"]) = err_elem "Illegal" chs
    1.17 +  | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
    1.18 +  | check_elem chs =
    1.19 +      (case ["/", "\\", "$", ":"] inter_string chs of
    1.20 +        [] => chs
    1.21 +      | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
    1.22 +
    1.23 +val basic_elem = Basic o implode o check_elem;
    1.24 +val variable_elem = Variable o implode o check_elem;
    1.25  
    1.26  fun is_var (Variable _) = true
    1.27    | is_var _ = false;