changeset 61538 | bf4969660913 |
parent 61192 | 98eba31c51f8 |
child 61728 | 5f5ff1eab407 |
61537:f6bd97a587b7 | 61538:bf4969660913 |
---|---|
253 GUI_Thread.require {} |
253 GUI_Thread.require {} |
254 |
254 |
255 reset_blob() |
255 reset_blob() |
256 reset_bibtex() |
256 reset_bibtex() |
257 |
257 |
258 for (doc_view <- PIDE.document_views(buffer)) |
|
259 doc_view.rich_text_area.active_reset() |
|
260 |
|
258 if (clear) { |
261 if (clear) { |
259 pending_clear = true |
262 pending_clear = true |
260 pending.clear |
263 pending.clear |
261 } |
264 } |
262 pending += e |
265 pending += e |