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