void dismissEditor(EditorProvider editor) {
		if (editor != null) {
			editor.dispose();
		}
		editorList.remove(editor); // Should the remove happen here or via the EditorListener?
	}
Closes the data type editor for the indicated data type.
@param editor the editor to close.
Ghidra/Features/Base/src/main/java/ghidra/app/plugin/core/datamgr/editor/DataTypeEditorManager.java