equal
deleted
inserted
replaced
138 } |
138 } |
139 |
139 |
140 |
140 |
141 /* activation */ |
141 /* activation */ |
142 |
142 |
|
143 private val token_marker = new Isabelle_Token_Marker(this) |
|
144 |
143 def activate() |
145 def activate() |
144 { |
146 { |
145 buffer.setTokenMarker(new Isabelle_Token_Marker(this)) |
147 buffer.setTokenMarker(token_marker) |
146 buffer.addBufferListener(buffer_listener) |
148 buffer.addBufferListener(buffer_listener) |
147 buffer.propertiesChanged() |
149 buffer.propertiesChanged() |
148 |
150 |
149 edits_buffer += new Text_Edit(true, 0, buffer.getText(0, buffer.getLength)) |
151 edits_buffer += new Text_Edit(true, 0, buffer.getText(0, buffer.getLength)) |
150 edits_delay() |
152 edits_delay() |
|
153 } |
|
154 |
|
155 def refresh() |
|
156 { |
|
157 buffer.setTokenMarker(token_marker) |
151 } |
158 } |
152 |
159 |
153 def deactivate() |
160 def deactivate() |
154 { |
161 { |
155 buffer.setTokenMarker(buffer.getMode.getTokenMarker) |
162 buffer.setTokenMarker(buffer.getMode.getTokenMarker) |