disallow blanks, relevant for session_name / theory_name e.g. in build log files;
--- 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(_))
+ }
}