Close work editor closeWork is called

Fixes #1602
workcraft · May 17, 2024 · 51dc91a · 51dc91a
1 parent 9342e87
commit 51dc91a
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 3 deletions.
diff --git a/workcraft/WorkcraftCore/src/org/workcraft/Framework.java b/workcraft/WorkcraftCore/src/org/workcraft/Framework.java
@@ -656,15 +656,21 @@ public void mergeWork(WorkspaceEntry we, File file) throws DeserialisationExcept
      */
     @SuppressWarnings("unused")
     public void closeWork(WorkspaceEntry we) {
-        getWorkspace().removeWork(we);
+        if ((we != null) && (mainWindow != null)) {
+            we.setChanged(false);
+            mainWindow.closeEditor(we);
+        }
+        if (we != null) {
+            workspace.removeWork(we);
+        }
     }
 
     /**
      * Used in core-workspace.js JavaScript wrapper.
      */
     @SuppressWarnings("unused")
     public void closeAllWorks() {
-        for (WorkspaceEntry we : getWorkspace().getWorks()) {
+        for (WorkspaceEntry we : workspace.getWorks()) {
             closeWork(we);
         }
     }

diff --git a/workcraft/WorkcraftCore/src/org/workcraft/gui/MainWindow.java b/workcraft/WorkcraftCore/src/org/workcraft/gui/MainWindow.java
@@ -317,7 +317,7 @@ private void closeDockableEditorWindow(DockableWindow window, GraphEditor editor
                 toggleDockableWindowMaximized(window);
             }
             DockableWindow dockableWindow = weWindowMap.remove(we);
-            // Close the work it has no associated windows, or clear listeners otherwise
+            // Close the work if it has no associated windows, or clear listeners otherwise
             if (dockableWindow == null) {
                 Framework.getInstance().closeWork(we);
             } else {

diff --git a/workcraft/WorkcraftCore/src/org/workcraft/workspace/Workspace.java b/workcraft/WorkcraftCore/src/org/workcraft/workspace/Workspace.java
@@ -117,6 +117,12 @@ public void addMount(Path<String> path, File file, boolean temporary) {
         fireWorkspaceChanged();
     }
 
+    public void removeMount(Path<String> path) {
+        mounts.remove(path);
+        permanentMounts.remove(path);
+
+    }
+
     public void fireWorkspaceChanged() {
         // TODO : categorise and route events
         for (WorkspaceListener listener : workspaceListeners) {