author | wenzelm |
Tue, 20 Jan 2009 22:29:56 +0100 | |
changeset 34493 | 0ffbc5ce9654 |
parent 34492 | 2268cbe29fca |
child 34494 | 47f9303db81d |
--- a/src/Tools/jEdit/src/proofdocument/Text.scala Tue Jan 20 22:29:41 2009 +0100 +++ b/src/Tools/jEdit/src/proofdocument/Text.scala Tue Jan 20 22:29:56 2009 +0100 @@ -8,7 +8,7 @@ object Text { - class Changed(val start: Int, val added: Int, val removed: Int) + case class Changed(val start: Int, val added: Int, val removed: Int) } trait Text {