changeset 66915 | f4259adc928a |
parent 66914 | fb3f13a9c756 |
child 67132 | 336831647779 |
--- 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(_)) + } }