--- a/src/Pure/Isar/parse.scala Thu Mar 15 14:13:49 2012 +0100
+++ b/src/Pure/Isar/parse.scala Thu Mar 15 14:22:54 2012 +0100
@@ -53,6 +53,7 @@
atom(Token.Kind.KEYWORD.toString + " " + quote(name),
tok => tok.kind == Token.Kind.KEYWORD && tok.content == name)
+ def string: Parser[String] = atom("string", _.is_string)
def name: Parser[String] = atom("name declaration", _.is_name)
def xname: Parser[String] = atom("name reference", _.is_xname)
def text: Parser[String] = atom("text", _.is_text)
--- a/src/Pure/Isar/token.scala Thu Mar 15 14:13:49 2012 +0100
+++ b/src/Pure/Isar/token.scala Thu Mar 15 14:22:54 2012 +0100
@@ -70,6 +70,7 @@
kind == Token.Kind.ALT_STRING ||
kind == Token.Kind.VERBATIM ||
kind == Token.Kind.COMMENT
+ def is_string: Boolean = kind == Token.Kind.STRING
def is_name: Boolean =
kind == Token.Kind.IDENT ||
kind == Token.Kind.SYM_IDENT ||
--- a/src/Pure/Thy/thy_header.ML Thu Mar 15 14:13:49 2012 +0100
+++ b/src/Pure/Thy/thy_header.ML Thu Mar 15 14:22:54 2012 +0100
@@ -81,7 +81,7 @@
val keyword_kind = Parse.group (fn () => "outer syntax keyword kind") (Parse.name -- Parse.tags);
val keyword_decl =
- Scan.repeat1 Parse.name -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_kind) >>
+ Scan.repeat1 Parse.string -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_kind) >>
(fn (names, kind) => map (rpair kind) names);
val keyword_decls = Parse.and_list1 keyword_decl >> flat;
--- a/src/Pure/Thy/thy_header.scala Thu Mar 15 14:13:49 2012 +0100
+++ b/src/Pure/Thy/thy_header.scala Thu Mar 15 14:22:54 2012 +0100
@@ -51,7 +51,7 @@
val keyword_kind =
atom("outer syntax keyword kind", _.is_name) ~ tags ^^ { case x ~ y => (x, y) }
val keyword_decl =
- rep1(name) ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^
+ rep1(string) ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^
{ case xs ~ y => xs.map((_, y)) }
val keyword_decls =
keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^