src/Pure/Isar/token.scala
changeset 55494 009b71c1ed23
parent 55492 28d4db6c6e79
child 55497 c0f8aebfb43d
     1.1 --- a/src/Pure/Isar/token.scala	Fri Feb 14 16:11:14 2014 +0100
     1.2 +++ b/src/Pure/Isar/token.scala	Fri Feb 14 16:25:30 2014 +0100
     1.3 @@ -34,6 +34,91 @@
     1.4    }
     1.5  
     1.6  
     1.7 +  /* parsers */
     1.8 +
     1.9 +  object Parsers extends Parsers
    1.10 +
    1.11 +  trait Parsers extends Scan.Parsers
    1.12 +  {
    1.13 +    private def delimited_token: Parser[Token] =
    1.14 +    {
    1.15 +      val string = quoted("\"") ^^ (x => Token(Token.Kind.STRING, x))
    1.16 +      val alt_string = quoted("`") ^^ (x => Token(Token.Kind.ALT_STRING, x))
    1.17 +      val verb = verbatim ^^ (x => Token(Token.Kind.VERBATIM, x))
    1.18 +      val cart = cartouche ^^ (x => Token(Token.Kind.CARTOUCHE, x))
    1.19 +      val cmt = comment ^^ (x => Token(Token.Kind.COMMENT, x))
    1.20 +
    1.21 +      string | (alt_string | (verb | (cart | cmt)))
    1.22 +    }
    1.23 +
    1.24 +    private def other_token(lexicon: Scan.Lexicon, is_command: String => Boolean)
    1.25 +      : Parser[Token] =
    1.26 +    {
    1.27 +      val letdigs1 = many1(Symbol.is_letdig)
    1.28 +      val sub = one(s => s == Symbol.sub_decoded || s == "\\<^sub>")
    1.29 +      val id =
    1.30 +        one(Symbol.is_letter) ~
    1.31 +          (rep(letdigs1 | (sub ~ letdigs1 ^^ { case x ~ y => x + y })) ^^ (_.mkString)) ^^
    1.32 +        { case x ~ y => x + y }
    1.33 +
    1.34 +      val nat = many1(Symbol.is_digit)
    1.35 +      val natdot = nat ~ "." ~ nat ^^ { case x ~ y ~ z => x + y + z }
    1.36 +      val id_nat = id ~ opt("." ~ nat) ^^ { case x ~ Some(y ~ z) => x + y + z case x ~ None => x }
    1.37 +
    1.38 +      val ident = id ~ rep("." ~> id) ^^
    1.39 +        { case x ~ Nil => Token(Token.Kind.IDENT, x)
    1.40 +          case x ~ ys => Token(Token.Kind.LONG_IDENT, (x :: ys).mkString(".")) }
    1.41 +
    1.42 +      val var_ = "?" ~ id_nat ^^ { case x ~ y => Token(Token.Kind.VAR, x + y) }
    1.43 +      val type_ident = "'" ~ id ^^ { case x ~ y => Token(Token.Kind.TYPE_IDENT, x + y) }
    1.44 +      val type_var = "?'" ~ id_nat ^^ { case x ~ y => Token(Token.Kind.TYPE_VAR, x + y) }
    1.45 +      val nat_ = nat ^^ (x => Token(Token.Kind.NAT, x))
    1.46 +      val float =
    1.47 +        ("-" ~ natdot ^^ { case x ~ y => x + y } | natdot) ^^ (x => Token(Token.Kind.FLOAT, x))
    1.48 +
    1.49 +      val sym_ident =
    1.50 +        (many1(Symbol.is_symbolic_char) | one(sym => Symbol.is_symbolic(sym))) ^^
    1.51 +        (x => Token(Token.Kind.SYM_IDENT, x))
    1.52 +
    1.53 +      val command_keyword =
    1.54 +        keyword(lexicon) ^^
    1.55 +          (x => Token(if (is_command(x)) Token.Kind.COMMAND else Token.Kind.KEYWORD, x))
    1.56 +
    1.57 +      val space = many1(Symbol.is_blank) ^^ (x => Token(Token.Kind.SPACE, x))
    1.58 +
    1.59 +      val recover_delimited =
    1.60 +        (recover_quoted("\"") |
    1.61 +          (recover_quoted("`") |
    1.62 +            (recover_verbatim |
    1.63 +              (recover_cartouche | recover_comment)))) ^^ (x => Token(Token.Kind.ERROR, x))
    1.64 +
    1.65 +      val bad = one(_ => true) ^^ (x => Token(Token.Kind.ERROR, x))
    1.66 +
    1.67 +      space | (recover_delimited |
    1.68 +        (((ident | (var_ | (type_ident | (type_var | (float | (nat_ | sym_ident)))))) |||
    1.69 +          command_keyword) | bad))
    1.70 +    }
    1.71 +
    1.72 +    def token(lexicon: Scan.Lexicon, is_command: String => Boolean): Parser[Token] =
    1.73 +      delimited_token | other_token(lexicon, is_command)
    1.74 +
    1.75 +    def token_context(lexicon: Scan.Lexicon, is_command: String => Boolean, ctxt: Scan.Context)
    1.76 +      : Parser[(Token, Scan.Context)] =
    1.77 +    {
    1.78 +      val string =
    1.79 +        quoted_context("\"", ctxt) ^^ { case (x, c) => (Token(Token.Kind.STRING, x), c) }
    1.80 +      val alt_string =
    1.81 +        quoted_context("`", ctxt) ^^ { case (x, c) => (Token(Token.Kind.ALT_STRING, x), c) }
    1.82 +      val verb = verbatim_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.VERBATIM, x), c) }
    1.83 +      val cart = cartouche_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.CARTOUCHE, x), c) }
    1.84 +      val cmt = comment_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.COMMENT, x), c) }
    1.85 +      val other = other_token(lexicon, is_command) ^^ { case x => (x, Scan.Finished) }
    1.86 +
    1.87 +      string | (alt_string | (verb | (cart | (cmt | other))))
    1.88 +    }
    1.89 +  }
    1.90 +
    1.91 +
    1.92    /* token reader */
    1.93  
    1.94    class Position(val line: Int, val file: String) extends scala.util.parsing.input.Position