src/Pure/Isar/token.scala
changeset 65335 7634d33c1a79
parent 64824 330ec9bc4b75
child 65523 4f2954adc217
equal deleted inserted replaced
65334:264a3904ab5a 65335:7634d33c1a79
   216     def atEnd = tokens.isEmpty
   216     def atEnd = tokens.isEmpty
   217   }
   217   }
   218 
   218 
   219   def reader(tokens: List[Token], start: Token.Pos): Reader =
   219   def reader(tokens: List[Token], start: Token.Pos): Reader =
   220     new Token_Reader(tokens, start)
   220     new Token_Reader(tokens, start)
       
   221 
       
   222 
       
   223   /* XML data representation */
       
   224 
       
   225   val encode: XML.Encode.T[Token] = (tok: Token) =>
       
   226   {
       
   227     import XML.Encode._
       
   228     pair(int, string)(tok.kind.id, tok.source)
       
   229   }
       
   230 
       
   231   val decode: XML.Decode.T[Token] = (body: XML.Body) =>
       
   232   {
       
   233     import XML.Decode._
       
   234     val (k, s) = pair(int, string)(body)
       
   235     Token(Kind(k), s)
       
   236   }
   221 }
   237 }
   222 
   238 
   223 
   239 
   224 sealed case class Token(kind: Token.Kind.Value, source: String)
   240 sealed case class Token(kind: Token.Kind.Value, source: String)
   225 {
   241 {