# HG changeset patch
# User wenzelm
# Date 1546188273 -3600
# Node ID b85f4c5cb58882ed6c47933138376e6182a3ff29
# Parent  27dae626822b664bc4d8379c5789bf154b80c5a0# Parent  adb52af5ba55bb51d7bedfc6da300d7153005f8d
merged

diff -r 27dae626822b -r b85f4c5cb588 src/Doc/Isar_Ref/Outer_Syntax.thy
--- 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>
 
 
diff -r 27dae626822b -r b85f4c5cb588 src/Pure/General/path.ML
--- 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
 
diff -r 27dae626822b -r b85f4c5cb588 src/Pure/General/path.scala
--- 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)))
 }
 
 
diff -r 27dae626822b -r b85f4c5cb588 src/Pure/Isar/token.scala
--- 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)
   }
 }