--- a/src/Pure/Isar/token.scala Thu Apr 20 11:38:42 2017 +0200
+++ b/src/Pure/Isar/token.scala Thu Apr 20 14:59:57 2017 +0200
@@ -152,6 +152,19 @@
val newline: Token = explode(Keyword.Keywords.empty, "\n").head
+ /* names */
+
+ def read_name(keywords: Keyword.Keywords, inp: CharSequence): Option[Token] =
+ explode(keywords, inp) match {
+ case List(tok) if tok.is_name => Some(tok)
+ case _ => None
+ }
+
+ def quote_name(keywords: Keyword.Keywords, name: String): String =
+ if (read_name(keywords, name).isDefined) name
+ else quote(name.replace("\"", "\\\""))
+
+
/* implode */
def implode(toks: List[Token]): String =