--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Sun Dec 30 10:34:56 2018 +0000
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Sun Dec 30 17:44:33 2018 +0100
@@ -189,7 +189,9 @@
\<close>}
A @{syntax_def system_name} is like @{syntax name}, but it excludes
- white-space characters and needs to conform to file-name notation.
+ white-space characters and needs to conform to file-name notation. Name
+ components that are special on Windows (e.g.\ \<^verbatim>\<open>CON\<close>, \<^verbatim>\<open>PRN\<close>, \<^verbatim>\<open>AUX\<close>) are
+ excluded on all platforms.
\<close>
--- a/src/Pure/General/path.ML Sun Dec 30 10:34:56 2018 +0000
+++ b/src/Pure/General/path.ML Sun Dec 30 17:44:33 2018 +0100
@@ -51,18 +51,20 @@
local
-fun err_elem msg s = error (msg ^ " path element specification " ^ quote s);
+fun err_elem msg s = error (msg ^ " path element " ^ quote s);
-fun check_elem s =
- if s = "" orelse s = "~" orelse s = "~~" then err_elem "Illegal" s
+val illegal_elem = ["", "~", "~~", ".", ".."];
+val illegal_char = ["/", "\\", "$", ":", "\"", "'", "<", ">", "|", "?", "*"];
+
+val check_elem = tap (fn s =>
+ if member (op =) illegal_elem s then err_elem "Illegal" s
else
- let
- fun check c =
- if exists_string (fn c' => c = c') s then
- err_elem ("Illegal character " ^ quote c ^ " in") s
- else ();
- val _ = List.app check ["/", "\\", "$", ":", "\"", "'"];
- in s end;
+ (s, ()) |-> fold_string (fn c => fn () =>
+ 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 ()));
in
--- a/src/Pure/General/path.scala Sun Dec 30 10:34:56 2018 +0000
+++ b/src/Pure/General/path.scala Sun Dec 30 17:44:33 2018 +0100
@@ -24,14 +24,20 @@
private case object Parent extends Elem
private def err_elem(msg: String, s: String): Nothing =
- error(msg + " path element specification " + quote(s))
+ error(msg + " path element " + quote(s))
+
+ private val illegal_elem = Set("", "~", "~~", ".", "..")
+ private val illegal_char = "/\\$:\"'<>|?*"
private def check_elem(s: String): String =
- if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s)
+ if (illegal_elem.contains(s)) err_elem("Illegal", s)
else {
- "/\\$:\"'".iterator.foreach(c =>
- if (s.iterator.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
}
@@ -112,6 +118,17 @@
/* encode */
val encode: XML.Encode.T[Path] = (path => XML.Encode.string(path.implode))
+
+
+ /* reserved names */
+
+ private val reserved_windows: Set[String] =
+ Set("CON", "PRN", "AUX", "NUL",
+ "COM1", "COM2", "COM3", "COM4", "COM5", "COM6", "COM7", "COM8", "COM9",
+ "LPT1", "LPT2", "LPT3", "LPT4", "LPT5", "LPT6", "LPT7", "LPT8", "LPT9")
+
+ def is_reserved(name: String): Boolean =
+ Long_Name.explode(name).exists(a => reserved_windows.contains(Word.uppercase(a)))
}
--- a/src/Pure/Isar/token.scala Sun Dec 30 10:34:56 2018 +0000
+++ b/src/Pure/Isar/token.scala Sun Dec 30 17:44:33 2018 +0100
@@ -328,6 +328,8 @@
def is_system_name: Boolean =
{
val s = content
- is_name && Path.is_wellformed(s) && !s.exists(Symbol.is_ascii_blank(_))
+ is_name && Path.is_wellformed(s) &&
+ !s.exists(Symbol.is_ascii_blank(_)) &&
+ !Path.is_reserved(s)
}
}