equal
deleted
inserted
replaced
80 |
80 |
81 /* read -- lazy scanning */ |
81 /* read -- lazy scanning */ |
82 |
82 |
83 def read(reader: Reader[Char]): Thy_Header = |
83 def read(reader: Reader[Char]): Thy_Header = |
84 { |
84 { |
85 val token = Scan.Parsers.token(lexicon, _ => false) |
85 val token = Token.Parsers.token(lexicon, _ => false) |
86 val toks = new mutable.ListBuffer[Token] |
86 val toks = new mutable.ListBuffer[Token] |
87 |
87 |
88 @tailrec def scan_to_begin(in: Reader[Char]) |
88 @tailrec def scan_to_begin(in: Reader[Char]) |
89 { |
89 { |
90 token(in) match { |
90 token(in) match { |
91 case Scan.Parsers.Success(tok, rest) => |
91 case Token.Parsers.Success(tok, rest) => |
92 toks += tok |
92 toks += tok |
93 if (!tok.is_begin) scan_to_begin(rest) |
93 if (!tok.is_begin) scan_to_begin(rest) |
94 case _ => |
94 case _ => |
95 } |
95 } |
96 } |
96 } |