# HG changeset patch
# User wenzelm
# Date 1508924458 -7200
# Node ID f4259adc928a690a202800a1db4d840a450fd401
# Parent  fb3f13a9c756fc85293389930b2e02f15984db5c
disallow blanks, relevant for session_name / theory_name e.g. in build log files;

diff -r fb3f13a9c756 -r f4259adc928a src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Wed Oct 25 11:35:48 2017 +0200
+++ b/src/Pure/Isar/token.scala	Wed Oct 25 11:40:58 2017 +0200
@@ -306,5 +306,9 @@
     else if (kind == Token.Kind.COMMENT) Scan.Parsers.comment_content(source)
     else source
 
-  def is_system_name: Boolean = is_name && Path.is_wellformed(content)
+  def is_system_name: Boolean =
+  {
+    val s = content
+    is_name && Path.is_wellformed(s) && !s.exists(Symbol.is_ascii_blank(_))
+  }
 }