# HG changeset patch
# User wenzelm
# Date 918148390 -3600
# Node ID e8807883e3e30e623c119a2087423d91bd7ed2f7
# Parent  2b24cf477313c36766773e05bfc5b5394e366317
check_elem: allow ~, except for '~' and '~~';

diff -r 2b24cf477313 -r e8807883e3e3 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Thu Feb 04 18:12:26 1999 +0100
+++ b/src/Pure/General/path.ML	Thu Feb 04 18:13:10 1999 +0100
@@ -33,14 +33,17 @@
 
 datatype elem = Root | Parent | Basic of string | Variable of string;
 
-fun no_meta_chars chs =
-  (case ["/", "\\", "$", "~"] inter_string chs of
-    [] => chs
-  | bads => error ("Illegal character(s) " ^ commas_quote bads ^
-      " in path element specification: " ^ quote (implode chs)));
+fun err_elem msg chs = error (msg ^ " path element specification: " ^ quote (implode chs));
 
-val basic_elem = Basic o implode o no_meta_chars;
-val variable_elem = Variable o implode o no_meta_chars;
+fun check_elem (chs as ["~"]) = err_elem "Illegal" chs
+  | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
+  | check_elem chs =
+      (case ["/", "\\", "$", ":"] inter_string chs of
+        [] => chs
+      | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
+
+val basic_elem = Basic o implode o check_elem;
+val variable_elem = Variable o implode o check_elem;
 
 fun is_var (Variable _) = true
   | is_var _ = false;