1.1 --- a/src/Pure/General/scan.scala	Mon Dec 21 16:50:28 2009 +0000
     1.2 +++ b/src/Pure/General/scan.scala	Tue Dec 22 14:58:13 2009 +0100
     1.3 @@ -135,9 +135,9 @@
     1.4      }.named("keyword")
     1.5  
     1.6  
     1.7 -    /* symbols */
     1.8 +    /* symbol range */
     1.9  
    1.10 -    def symbols(pred: String => Boolean, min_count: Int, max_count: Int): Parser[String] =
    1.11 +    def symbol_range(pred: String => Boolean, min_count: Int, max_count: Int): Parser[String] =
    1.12        new Parser[String]
    1.13        {
    1.14          def apply(in: Input) =
    1.15 @@ -161,11 +161,11 @@
    1.16            if (count < min_count) Failure("bad input", in)
    1.17            else Success(in.source.subSequence(start, i).toString, in.drop(i - start))
    1.18          }
    1.19 -      }.named("symbols")
    1.20 +      }.named("symbol_range")
    1.21  
    1.22 -    def one(pred: String => Boolean): Parser[String] = symbols(pred, 1, 1)
    1.23 -    def many(pred: String => Boolean): Parser[String] = symbols(pred, 0, Integer.MAX_VALUE)
    1.24 -    def many1(pred: String => Boolean): Parser[String] = symbols(pred, 1, Integer.MAX_VALUE)
    1.25 +    def one(pred: String => Boolean): Parser[String] = symbol_range(pred, 1, 1)
    1.26 +    def many(pred: String => Boolean): Parser[String] = symbol_range(pred, 0, Integer.MAX_VALUE)
    1.27 +    def many1(pred: String => Boolean): Parser[String] = symbol_range(pred, 1, Integer.MAX_VALUE)
    1.28  
    1.29  
    1.30      /* quoted strings */
    1.31 @@ -246,38 +246,41 @@
    1.32      def token(symbols: Symbol.Interpretation, is_command: String => Boolean):
    1.33        Parser[Outer_Lex.Token] =
    1.34      {
    1.35 -      import Outer_Lex._
    1.36 +      import Outer_Lex.Token_Kind, Outer_Lex.Token
    1.37  
    1.38        val id = one(symbols.is_letter) ~ many(symbols.is_letdig) ^^ { case x ~ y => x + y }
    1.39        val nat = many1(symbols.is_digit)
    1.40        val id_nat = id ~ opt("." ~ nat) ^^ { case x ~ Some(y ~ z) => x + y + z case x ~ None => x }
    1.41  
    1.42        val ident = id ~ rep("." ~> id) ^^
    1.43 -        { case x ~ Nil => Ident(x)
    1.44 -          case x ~ ys => Long_Ident((x :: ys).mkString(".")) }
    1.45 +        { case x ~ Nil => Token(Token_Kind.IDENT, x)
    1.46 +          case x ~ ys => Token(Token_Kind.LONG_IDENT, (x :: ys).mkString(".")) }
    1.47  
    1.48 -      val var_ = "?" ~ id_nat ^^ { case x ~ y => Var(x + y) }
    1.49 -      val type_ident = "'" ~ id ^^ { case x ~ y => Type_Ident(x + y) }
    1.50 -      val type_var = "?'" ~ id_nat ^^ { case x ~ y => Type_Var(x + y) }
    1.51 -      val nat_ = nat ^^ Nat
    1.52 +      val var_ = "?" ~ id_nat ^^ { case x ~ y => Token(Token_Kind.VAR, x + y) }
    1.53 +      val type_ident = "'" ~ id ^^ { case x ~ y => Token(Token_Kind.TYPE_IDENT, x + y) }
    1.54 +      val type_var = "?'" ~ id_nat ^^ { case x ~ y => Token(Token_Kind.TYPE_VAR, x + y) }
    1.55 +      val nat_ = nat ^^ (x => Token(Token_Kind.NAT, x))
    1.56  
    1.57        val sym_ident =
    1.58          (many1(symbols.is_symbolic_char) |
    1.59 -          one(sym => symbols.is_symbolic(sym) & Symbol.is_closed(sym))) ^^ Sym_Ident
    1.60 +          one(sym => symbols.is_symbolic(sym) & Symbol.is_closed(sym))) ^^
    1.61 +        (x => Token(Token_Kind.SYM_IDENT, x))
    1.62  
    1.63 -      val space = many1(symbols.is_blank) ^^ Space
    1.64 +      val space = many1(symbols.is_blank) ^^ (x => Token(Token_Kind.SPACE, x))
    1.65  
    1.66 -      val string = quoted("\"") ^^ String_Token
    1.67 -      val alt_string = quoted("`") ^^ Alt_String_Token
    1.68 +      val string = quoted("\"") ^^ (x => Token(Token_Kind.STRING, x))
    1.69 +      val alt_string = quoted("`") ^^ (x => Token(Token_Kind.ALT_STRING, x))
    1.70  
    1.71 -      val bad_input = many1(sym => !(symbols.is_blank(sym))) ^^ Bad_Input
    1.72 +      val bad_input = many1(sym => !(symbols.is_blank(sym))) ^^
    1.73 +        (x => Token(Token_Kind.BAD_INPUT, x))
    1.74  
    1.75  
    1.76        /* tokens */
    1.77  
    1.78 -      (space | (string | (alt_string | (verbatim ^^ Verbatim | comment ^^ Comment)))) |
    1.79 +      (space | (string | (alt_string | (verbatim ^^ (x => Token(Token_Kind.VERBATIM, x)) |
    1.80 +        comment ^^ (x => Token(Token_Kind.COMMENT, x)))))) |
    1.81        ((ident | (var_ | (type_ident | (type_var | (nat_ | sym_ident))))) |||
    1.82 -        keyword ^^ (x => if (is_command(x)) Command(x) else Keyword(x))) |
    1.83 +        keyword ^^ (x => Token(if (is_command(x)) Token_Kind.COMMAND else Token_Kind.KEYWORD, x))) |
    1.84        bad_input
    1.85      }
    1.86    }