# HG changeset patch
# User wenzelm
# Date 1546185391 -3600
# Node ID adb52af5ba55bb51d7bedfc6da300d7153005f8d
# Parent  57ff523d90089d64b4d2004e799c8d636817b81e
exclude file name components that are special on Windows;

diff -r 57ff523d9008 -r adb52af5ba55 src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Sun Dec 30 16:25:15 2018 +0100
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Sun Dec 30 16:56:31 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 57ff523d9008 -r adb52af5ba55 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Sun Dec 30 16:25:15 2018 +0100
+++ b/src/Pure/General/path.scala	Sun Dec 30 16:56:31 2018 +0100
@@ -118,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 57ff523d9008 -r adb52af5ba55 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Sun Dec 30 16:25:15 2018 +0100
+++ b/src/Pure/Isar/token.scala	Sun Dec 30 16:56:31 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)
   }
 }