src/Pure/Thy/thy_header.scala
changeset 73368 894f29abe5fc
parent 73359 d8a0e996614b
equal deleted inserted replaced
73367:77ef8bef0593 73368:894f29abe5fc
   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