src/Pure/Isar/parse.scala

 
     def keyword(name: String): Parser[String] =
       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)
     def ML_source: Parser[String] = atom("ML source", _.is_text)
     def doc_source: Parser[String] = atom("document source", _.is_text)