| changeset 34539 | 5d88e0681d44 |
| parent 34531 | db1c28e326fc |
| parent 34533 | 35308320713a |
| child 34551 | bd2b8fde9e25 |
--- a/src/Tools/jEdit/src/proofdocument/Token.scala Thu Mar 19 16:18:57 2009 +0100 +++ b/src/Tools/jEdit/src/proofdocument/Token.scala Thu Mar 19 16:48:29 2009 +0100 @@ -42,5 +42,6 @@ val length = content.length val stop = start + length override def toString = content + "(" + kind + ")" + override def hashCode: Int = (31 + start) * 31 + stop def shift(i: Int) = new Token(start + i, content, kind) }