equal
deleted
inserted
replaced
122 { |
122 { |
123 def insert(start: Offset, text: String): Edit = new Edit(true, start, text) |
123 def insert(start: Offset, text: String): Edit = new Edit(true, start, text) |
124 def remove(start: Offset, text: String): Edit = new Edit(false, start, text) |
124 def remove(start: Offset, text: String): Edit = new Edit(false, start, text) |
125 } |
125 } |
126 |
126 |
127 class Edit(val is_insert: Boolean, val start: Offset, val text: String) |
127 class Edit private(val is_insert: Boolean, val start: Offset, val text: String) |
128 { |
128 { |
129 override def toString = |
129 override def toString = |
130 (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")" |
130 (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")" |
131 |
131 |
132 |
132 |