equal
deleted
inserted
replaced
211 case Success(result, _) => result |
211 case Success(result, _) => result |
212 case bad => error(bad.toString) |
212 case bad => error(bad.toString) |
213 } |
213 } |
214 } |
214 } |
215 |
215 |
216 def read(reader: Reader[Char], start: Token.Pos, strict: Boolean = true): Thy_Header = |
216 def read(reader: Reader[Char], |
|
217 start: Token.Pos = Token.Pos.none, |
|
218 strict: Boolean = true): Thy_Header = |
217 { |
219 { |
218 val (_, tokens0) = read_tokens(reader, true) |
220 val (_, tokens0) = read_tokens(reader, true) |
219 val text = Scan.reader_decode_utf8(reader, Token.implode(tokens0)) |
221 val text = Scan.reader_decode_utf8(reader, Token.implode(tokens0)) |
220 |
222 |
221 val (drop_tokens, tokens) = read_tokens(Scan.char_reader(text), strict) |
223 val (drop_tokens, tokens) = read_tokens(Scan.char_reader(text), strict) |