| changeset 52507 | 27925b58d6bd |
| parent 51496 | cb677987b7e3 |
| child 52509 | 2193d2c7f586 |
--- a/src/Pure/PIDE/command.scala Tue Jul 02 20:47:32 2013 +0200 +++ b/src/Pure/PIDE/command.scala Wed Jul 03 15:11:15 2013 +0200 @@ -227,7 +227,7 @@ def source(range: Text.Range): String = source.substring(range.start, range.stop) - lazy val symbol_index = new Symbol.Index(source) + lazy val symbol_index = Symbol.Index(source) def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i) def decode(r: Text.Range): Text.Range = symbol_index.decode(r)