changeset 49414 | d7b5fb2e9ca2 |
parent 45455 | 4f974c0c5c2f |
--- a/src/Pure/PIDE/blob.scala Tue Sep 18 11:49:23 2012 +0200 +++ b/src/Pure/PIDE/blob.scala Tue Sep 18 13:18:45 2012 +0200 @@ -24,5 +24,5 @@ def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i) def decode(r: Text.Range): Text.Range = symbol_index.decode(r) - val empty_state: Blob.State = Blob.State(this) + val init_state: Blob.State = Blob.State(this) }