1.1 --- a/src/Pure/General/path.ML	Sat Jul 21 17:49:22 2012 +0200
     1.2 +++ b/src/Pure/General/path.ML	Sat Jul 21 21:16:08 2012 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4    | check_elem (chs as ["~"]) = err_elem "Illegal" chs
     1.5    | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
     1.6    | check_elem chs =
     1.7 -      (case inter (op =) ["/", "\\", ":"] chs of
     1.8 +      (case inter (op =) ["/", "\\", "$", ":", "\"", "'"] chs of
     1.9          [] => chs
    1.10        | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
    1.11  

     2.1 --- a/src/Pure/General/path.scala	Sat Jul 21 17:49:22 2012 +0200
     2.2 +++ b/src/Pure/General/path.scala	Sat Jul 21 21:16:08 2012 +0200
     2.3 @@ -29,7 +29,8 @@
     2.4    private def check_elem(s: String): String =
     2.5      if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s)
     2.6      else
     2.7 -      s.iterator.filter(c => c == '/' || c == '\\' || c == '$' || c == ':').toList match {
     2.8 +      s.iterator.filter(c =>
     2.9 +          c == '/' || c == '\\' || c == '$' || c == ':' || c == '"' || c == '\'').toList match {
    2.10          case Nil => s
    2.11          case bads =>
    2.12            err_elem ("Illegal character(s) " + commas_quote(bads.map(_.toString)) + " in", s)