# HG changeset patch
# User wenzelm
# Date 1232486996 -3600
# Node ID 0ffbc5ce96545134879c47e6dd7becbfa8d9ff18
# Parent  2268cbe29fca78f295cf3e1497f6eae6960d5568
case class Changed;

diff -r 2268cbe29fca -r 0ffbc5ce9654 src/Tools/jEdit/src/proofdocument/Text.scala
--- 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 {