equal
deleted
inserted
replaced
184 /* read -- lazy scanning */ |
184 /* read -- lazy scanning */ |
185 |
185 |
186 private def read_tokens(reader: Reader[Char], strict: Boolean): (List[Token], List[Token]) = |
186 private def read_tokens(reader: Reader[Char], strict: Boolean): (List[Token], List[Token]) = |
187 { |
187 { |
188 val token = Token.Parsers.token(bootstrap_keywords) |
188 val token = Token.Parsers.token(bootstrap_keywords) |
189 def make_tokens(in: Reader[Char]): Stream[Token] = |
189 def make_tokens(in: Reader[Char]): LazyList[Token] = |
190 token(in) match { |
190 token(in) match { |
191 case Token.Parsers.Success(tok, rest) => tok #:: make_tokens(rest) |
191 case Token.Parsers.Success(tok, rest) => tok #:: make_tokens(rest) |
192 case _ => Stream.empty |
192 case _ => LazyList.empty |
193 } |
193 } |
194 |
194 |
195 val all_tokens = make_tokens(reader) |
195 val all_tokens = make_tokens(reader) |
196 val drop_tokens = |
196 val drop_tokens = |
197 if (strict) Nil |
197 if (strict) Nil |