function closeFullEditor(file) {
        // If this was the current document shown in the editor UI, we're going to switch to a
        // different document (or none if working set has no other options)
        if (_currentDocument && _currentDocument.file.fullPath === file.fullPath) {
            var wsIndex = findInWorkingSet(file.fullPath);
            
            // Decide which doc to show in editor after this one
            var nextFile;
            if (wsIndex === -1) {
                // If doc wasn't in working set, use bottommost working set item
                if (_workingSet.length > 0) {
                    nextFile = _workingSet[_workingSet.length  - 1];
                }
                // else: leave nextDocument null; editor area will be blank
            } else {
                // If doc was in working set, use item next to it (below if possible)
                if (wsIndex < _workingSet.length - 1) {
                    nextFile = _workingSet[wsIndex + 1];
                } else if (wsIndex > 0) {
                    nextFile = _workingSet[wsIndex - 1];
                }
                // else: leave nextDocument null; editor area will be blank
            }
            
            // Switch editor to next document (or blank it out)
            if (nextFile) {
                CommandManager.execute(Commands.FILE_OPEN, { fullPath: nextFile.fullPath });
            } else {
                _clearCurrentDocument();
            }
        }
        
        // (Now we're guaranteed that the current document is not the one we're closing)
        console.assert(!(_currentDocument && _currentDocument.file.fullPath === file.fullPath));
        
        // Remove closed doc from working set, if it was in there
        // This happens regardless of whether the document being closed was the current one or not
        removeFromWorkingSet(file);
        
        // Note: EditorManager will dispose the closed document's now-unneeded editor either in
        // response to the editor-swap call above, or the removeFromWorkingSet() call, depending on
        // circumstances. See notes in EditorManager for more.
    }
Closes the full editor for the given file (if there is one), and removes it from the working
set. Any other editors for this Document remain open. Discards any unsaved changes - it is
expected that the UI has already confirmed with the user before calling this.

Changes currentDocument if this file was the current document (may change to null).

This is a subset of notifyFileDeleted(). Use this for the user-facing Close command.

@param {!FileEntry} file