| commit | b36656260dfd846c4078815363263ab97307f96f | [log] [tgz] |
|---|---|---|
| author | Florian Thienel <florian@thienel.org> | Thu Jan 28 19:28:45 2016 +0100 |
| committer | Florian Thienel <florian@thienel.org> | Thu Jan 28 19:28:45 2016 +0100 |
| tree | 2fe706733613198ddf6d40bc230e13e1a44e83b7 | |
| parent | 9d53249b1cda94482f2ece39ca5e857419683a0c [diff] |
flush the style cache when an editor is closed Signed-off-by: Florian Thienel <florian@thienel.org>
diff --git a/org.eclipse.vex.ui/src/org/eclipse/vex/ui/internal/editor/VexEditor.java b/org.eclipse.vex.ui/src/org/eclipse/vex/ui/internal/editor/VexEditor.java index 05c725f..9d4bc69 100644 --- a/org.eclipse.vex.ui/src/org/eclipse/vex/ui/internal/editor/VexEditor.java +++ b/org.eclipse.vex.ui/src/org/eclipse/vex/ui/internal/editor/VexEditor.java
@@ -233,6 +233,10 @@ document.removeDocumentListener(documentListener); } + if (style != null) { + style.getStyleSheet().flushAllStyles(document); + } + getEditorSite().getSelectionProvider().removeSelectionChangedListener(selectionChangedListener); if (parentControl != null) {