# HG changeset patch
# User wenzelm
# Date 1331817774 -3600
# Node ID ac1c41ea856d4a8458e2ade5ec67651dc6ff6100
# Parent  f5c2d66faa041b633762a48c60bfcbd0a1ecb2c8
clarified syntax of prospective keywords;

diff -r f5c2d66faa04 -r ac1c41ea856d src/Pure/Isar/parse.scala
--- 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)
diff -r f5c2d66faa04 -r ac1c41ea856d src/Pure/Isar/token.scala
--- 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 ||
diff -r f5c2d66faa04 -r ac1c41ea856d src/Pure/Thy/thy_header.ML
--- 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;
 
diff -r f5c2d66faa04 -r ac1c41ea856d src/Pure/Thy/thy_header.scala
--- 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 }) ^^