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) {