# HG changeset patch
# User wenzelm
# Date 1546183515 -3600
# Node ID 57ff523d90089d64b4d2004e799c8d636817b81e
# Parent  612a02019f489938b1c0db7abc4301933fef4ddf
reject further illegal chars according to https://docs.microsoft.com/en-us/windows/desktop/fileio/naming-a-file

diff -r 612a02019f48 -r 57ff523d9008 src/Pure/General/path.ML
--- 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 ()));
 
diff -r 612a02019f48 -r 57ff523d9008 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Sun Dec 30 16:06:09 2018 +0100
+++ b/src/Pure/General/path.scala	Sun Dec 30 16:25:15 2018 +0100
@@ -27,13 +27,16 @@
     error(msg + " path element " + quote(s))
 
   private val illegal_elem = Set("", "~", "~~", ".", "..")
-  private val illegal_char = "/\\$:\"'"
+  private val illegal_char = "/\\$:\"'<>|?*"
 
   private def check_elem(s: String): String =
     if (illegal_elem.contains(s)) err_elem("Illegal", s)
     else {
-      for (c <- s if illegal_char.contains(c)) {
-        err_elem("Illegal character " + quote(c.toString) + " in", s)
+      for (c <- s) {
+        if (c.toInt < 32)
+          err_elem("Illegal control character " + c.toInt + " in", s)
+        if (illegal_char.contains(c))
+          err_elem("Illegal character " + quote(c.toString) + " in", s)
       }
       s
     }