[375507] deleting a server with a dirty server editor - prompt for closing serve editor during server editor.
diff --git a/plugins/org.eclipse.wst.server.ui/serverui/org/eclipse/wst/server/ui/internal/editor/ServerEditor.java b/plugins/org.eclipse.wst.server.ui/serverui/org/eclipse/wst/server/ui/internal/editor/ServerEditor.java
index f9723a1..7b62517 100644
--- a/plugins/org.eclipse.wst.server.ui/serverui/org/eclipse/wst/server/ui/internal/editor/ServerEditor.java
+++ b/plugins/org.eclipse.wst.server.ui/serverui/org/eclipse/wst/server/ui/internal/editor/ServerEditor.java
@@ -99,6 +99,12 @@
resourceDeleted = true;
if (!isDirty()) {
closeEditor();
+ } else {
+ Display.getDefault().asyncExec(new Runnable() {
+ public void run() {
+ checkAndCloseEditorOnDeletedServer();
+ }
+ });
}
}
}
@@ -932,16 +938,7 @@
super.setFocus();
}
- /**
- *
- */
- protected void checkResourceState() {
- // do not check the resource state change if saving through the editor
- if (isSaving) {
- // do nothing
- return;
- }
-
+ void checkAndCloseEditorOnDeletedServer() {
// check for deleted files
if (resourceDeleted) {
String title = Messages.editorResourceDeleteTitle;
@@ -955,10 +952,24 @@
doSave(new NullProgressMonitor());
else
closeEditor();
- return;
}
resourceDeleted = false;
+ }
+
+
+ /**
+ *
+ */
+ protected void checkResourceState() {
+ // do not check the resource state change if saving through the editor
+ if (isSaving) {
+ // do nothing
+ return;
+ }
+ // check for deleted files
+ checkAndCloseEditorOnDeletedServer();
+
// check for server changes
if (serverId != null) {
if (!commandManager.isDirty(serverId)) {
