equal
deleted
inserted
replaced
73 |
73 |
74 /* read -- lazy scanning */ |
74 /* read -- lazy scanning */ |
75 |
75 |
76 def read(reader: Reader[Char]): Header = |
76 def read(reader: Reader[Char]): Header = |
77 { |
77 { |
78 val token = lexicon.token(Isabelle_System.symbols, _ => false) |
78 val token = lexicon.token(_ => false) |
79 val toks = new mutable.ListBuffer[Token] |
79 val toks = new mutable.ListBuffer[Token] |
80 |
80 |
81 @tailrec def scan_to_begin(in: Reader[Char]) |
81 @tailrec def scan_to_begin(in: Reader[Char]) |
82 { |
82 { |
83 token(in) match { |
83 token(in) match { |