equal
deleted
inserted
replaced
10 import scala.collection.mutable |
10 import scala.collection.mutable |
11 |
11 |
12 |
12 |
13 object Thy_Syntax |
13 object Thy_Syntax |
14 { |
14 { |
15 type Span = List[Token] |
15 def parse_spans(toks: List[Token]): List[List[Token]] = |
16 |
|
17 def parse_spans(toks: List[Token]): List[Span] = |
|
18 { |
16 { |
19 val result = new mutable.ListBuffer[Span] |
17 val result = new mutable.ListBuffer[List[Token]] |
20 val span = new mutable.ListBuffer[Token] |
18 val span = new mutable.ListBuffer[Token] |
21 val whitespace = new mutable.ListBuffer[Token] |
19 val whitespace = new mutable.ListBuffer[Token] |
22 |
20 |
23 def flush(buffer: mutable.ListBuffer[Token]) |
21 def flush(buffer: mutable.ListBuffer[Token]) |
24 { |
22 { |