src/Pure/Isar/token.scala

--- a/src/Pure/Isar/token.scala	Fri Feb 14 16:11:14 2014 +0100
+++ b/src/Pure/Isar/token.scala	Fri Feb 14 16:25:30 2014 +0100
@@ -34,6 +34,91 @@
   }
 
 
+  /* parsers */
+
+  object Parsers extends Parsers
+
+  trait Parsers extends Scan.Parsers
+  {
+    private def delimited_token: Parser[Token] =
+    {
+      val string = quoted("\"") ^^ (x => Token(Token.Kind.STRING, x))
+      val alt_string = quoted("`") ^^ (x => Token(Token.Kind.ALT_STRING, x))
+      val verb = verbatim ^^ (x => Token(Token.Kind.VERBATIM, x))
+      val cart = cartouche ^^ (x => Token(Token.Kind.CARTOUCHE, x))
+      val cmt = comment ^^ (x => Token(Token.Kind.COMMENT, x))
+
+      string | (alt_string | (verb | (cart | cmt)))
+    }
+
+    private def other_token(lexicon: Scan.Lexicon, is_command: String => Boolean)
+      : Parser[Token] =
+    {
+      val letdigs1 = many1(Symbol.is_letdig)
+      val sub = one(s => s == Symbol.sub_decoded || s == "\\<^sub>")
+      val id =
+        one(Symbol.is_letter) ~
+          (rep(letdigs1 | (sub ~ letdigs1 ^^ { case x ~ y => x + y })) ^^ (_.mkString)) ^^
+        { case x ~ y => x + y }
+
+      val nat = many1(Symbol.is_digit)
+      val natdot = nat ~ "." ~ nat ^^ { case x ~ y ~ z => x + y + z }
+      val id_nat = id ~ opt("." ~ nat) ^^ { case x ~ Some(y ~ z) => x + y + z case x ~ None => x }
+
+      val ident = id ~ rep("." ~> id) ^^
+        { case x ~ Nil => Token(Token.Kind.IDENT, x)
+          case x ~ ys => Token(Token.Kind.LONG_IDENT, (x :: ys).mkString(".")) }
+
+      val var_ = "?" ~ id_nat ^^ { case x ~ y => Token(Token.Kind.VAR, x + y) }
+      val type_ident = "'" ~ id ^^ { case x ~ y => Token(Token.Kind.TYPE_IDENT, x + y) }
+      val type_var = "?'" ~ id_nat ^^ { case x ~ y => Token(Token.Kind.TYPE_VAR, x + y) }
+      val nat_ = nat ^^ (x => Token(Token.Kind.NAT, x))
+      val float =
+        ("-" ~ natdot ^^ { case x ~ y => x + y } | natdot) ^^ (x => Token(Token.Kind.FLOAT, x))
+
+      val sym_ident =
+        (many1(Symbol.is_symbolic_char) | one(sym => Symbol.is_symbolic(sym))) ^^
+        (x => Token(Token.Kind.SYM_IDENT, x))
+
+      val command_keyword =
+        keyword(lexicon) ^^
+          (x => Token(if (is_command(x)) Token.Kind.COMMAND else Token.Kind.KEYWORD, x))
+
+      val space = many1(Symbol.is_blank) ^^ (x => Token(Token.Kind.SPACE, x))
+
+      val recover_delimited =
+        (recover_quoted("\"") |
+          (recover_quoted("`") |
+            (recover_verbatim |
+              (recover_cartouche | recover_comment)))) ^^ (x => Token(Token.Kind.ERROR, x))
+
+      val bad = one(_ => true) ^^ (x => Token(Token.Kind.ERROR, x))
+
+      space | (recover_delimited |
+        (((ident | (var_ | (type_ident | (type_var | (float | (nat_ | sym_ident)))))) |||
+          command_keyword) | bad))
+    }
+
+    def token(lexicon: Scan.Lexicon, is_command: String => Boolean): Parser[Token] =
+      delimited_token | other_token(lexicon, is_command)
+
+    def token_context(lexicon: Scan.Lexicon, is_command: String => Boolean, ctxt: Scan.Context)
+      : Parser[(Token, Scan.Context)] =
+    {
+      val string =
+        quoted_context("\"", ctxt) ^^ { case (x, c) => (Token(Token.Kind.STRING, x), c) }
+      val alt_string =
+        quoted_context("`", ctxt) ^^ { case (x, c) => (Token(Token.Kind.ALT_STRING, x), c) }
+      val verb = verbatim_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.VERBATIM, x), c) }
+      val cart = cartouche_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.CARTOUCHE, x), c) }
+      val cmt = comment_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.COMMENT, x), c) }
+      val other = other_token(lexicon, is_command) ^^ { case x => (x, Scan.Finished) }
+
+      string | (alt_string | (verb | (cart | (cmt | other))))
+    }
+  }
+
+
   /* token reader */
 
   class Position(val line: Int, val file: String) extends scala.util.parsing.input.Position