equal
deleted
inserted
replaced
110 private val buffer_listener: BufferListener = new BufferAdapter |
110 private val buffer_listener: BufferListener = new BufferAdapter |
111 { |
111 { |
112 override def contentInserted(buffer: JEditBuffer, |
112 override def contentInserted(buffer: JEditBuffer, |
113 start_line: Int, offset: Int, num_lines: Int, length: Int) |
113 start_line: Int, offset: Int, num_lines: Int, length: Int) |
114 { |
114 { |
115 edits_buffer += Text_Edit.Insert(offset, buffer.getText(offset, length)) |
115 edits_buffer += new Text_Edit(true, offset, buffer.getText(offset, length)) |
116 edits_delay() |
116 edits_delay() |
117 } |
117 } |
118 |
118 |
119 override def preContentRemoved(buffer: JEditBuffer, |
119 override def preContentRemoved(buffer: JEditBuffer, |
120 start_line: Int, start: Int, num_lines: Int, removed_length: Int) |
120 start_line: Int, start: Int, num_lines: Int, removed_length: Int) |
121 { |
121 { |
122 edits_buffer += Text_Edit.Remove(start, buffer.getText(start, removed_length)) |
122 edits_buffer += new Text_Edit(false, start, buffer.getText(start, removed_length)) |
123 edits_delay() |
123 edits_delay() |
124 } |
124 } |
125 } |
125 } |
126 |
126 |
127 |
127 |
131 { |
131 { |
132 buffer.setTokenMarker(new Isabelle_Token_Marker(this)) |
132 buffer.setTokenMarker(new Isabelle_Token_Marker(this)) |
133 buffer.addBufferListener(buffer_listener) |
133 buffer.addBufferListener(buffer_listener) |
134 buffer.propertiesChanged() |
134 buffer.propertiesChanged() |
135 |
135 |
136 edits_buffer += Text_Edit.Insert(0, buffer.getText(0, buffer.getLength)) |
136 edits_buffer += new Text_Edit(true, 0, buffer.getText(0, buffer.getLength)) |
137 edits_delay() |
137 edits_delay() |
138 } |
138 } |
139 |
139 |
140 def deactivate() |
140 def deactivate() |
141 { |
141 { |