equal
deleted
inserted
replaced
22 |
22 |
23 lazy val symbol_index = new Symbol.Index(source) |
23 lazy val symbol_index = new Symbol.Index(source) |
24 def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i) |
24 def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i) |
25 def decode(r: Text.Range): Text.Range = symbol_index.decode(r) |
25 def decode(r: Text.Range): Text.Range = symbol_index.decode(r) |
26 |
26 |
27 val empty_state: Blob.State = Blob.State(this) |
27 val init_state: Blob.State = Blob.State(this) |
28 } |
28 } |