Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/General/path.ML
changeset 69550 57ff523d9008
parent 69549 612a02019f48
child 69627 3e26471d6d01 
--- a/src/Pure/General/path.ML	Sun Dec 30 16:06:09 2018 +0100
+++ b/src/Pure/General/path.ML	Sun Dec 30 16:25:15 2018 +0100
@@ -54,13 +54,15 @@
 fun err_elem msg s = error (msg ^ " path element " ^ quote s);
 
 val illegal_elem = ["", "~", "~~", ".", ".."];
-val illegal_char = ["/", "\\", "$", ":", "\"", "'"];
+val illegal_char = ["/", "\\", "$", ":", "\"", "'", "<", ">", "|", "?", "*"];
 
 val check_elem = tap (fn s =>
   if member (op =) illegal_elem s then err_elem "Illegal" s
   else
     (s, ()) |-> fold_string (fn c => fn () =>
-      if member (op =) illegal_char c then
+      if ord c < 32 then
+        err_elem ("Illegal control character " ^ string_of_int (ord c) ^ " in") s
+      else if member (op =) illegal_char c then
         err_elem ("Illegal character " ^ quote c ^ " in") s
       else ()));
isabelle