# HG changeset patch # User wenzelm # Date 1342898168 -7200 # Node ID a8ed41b6280bb31e8c444983d217595f2b31a907 # Parent 6d7b6e47f3efe3b02394b8b1da109a4482d3e49d disallow quotes in path specifications -- extra paranoia; diff -r 6d7b6e47f3ef -r a8ed41b6280b src/Pure/General/path.ML --- a/src/Pure/General/path.ML Sat Jul 21 17:49:22 2012 +0200 +++ b/src/Pure/General/path.ML Sat Jul 21 21:16:08 2012 +0200 @@ -51,7 +51,7 @@ | check_elem (chs as ["~"]) = err_elem "Illegal" chs | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs | check_elem chs = - (case inter (op =) ["/", "\\", ":"] chs of + (case inter (op =) ["/", "\\", "$", ":", "\"", "'"] chs of [] => chs | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs); diff -r 6d7b6e47f3ef -r a8ed41b6280b src/Pure/General/path.scala --- a/src/Pure/General/path.scala Sat Jul 21 17:49:22 2012 +0200 +++ b/src/Pure/General/path.scala Sat Jul 21 21:16:08 2012 +0200 @@ -29,7 +29,8 @@ private def check_elem(s: String): String = if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s) else - s.iterator.filter(c => c == '/' || c == '\\' || c == '$' || c == ':').toList match { + s.iterator.filter(c => + c == '/' || c == '\\' || c == '$' || c == ':' || c == '"' || c == '\'').toList match { case Nil => s case bads => err_elem ("Illegal character(s) " + commas_quote(bads.map(_.toString)) + " in", s)