public final class KeYFileChooser
extends javax.swing.JFileChooser
getFileChooser(String)
. This has the benefit of remembering the last visited directory
across different load/save actions of the user. To keep it simple, the choosable file filters
contain all file extensions that are relevant in KeY. The predefined constants can be used to
set the corresponding filter via JFileChooser.setFileFilter(FileFilter)
. Usually it is a good idea to
do this right after calling getFileChooser(String)
.javax.swing.JFileChooser.AccessibleJFileChooser
javax.swing.JComponent.AccessibleJComponent
Modifier and Type | Field and Description |
---|---|
static javax.swing.filechooser.FileFilter |
COMPRESSED_FILTER
filter for compressed proof files
|
static javax.swing.filechooser.FileFilter |
DEFAULT_FILTER
default file filter for loading files
|
static javax.swing.filechooser.FileFilter |
INTERACTION_LOG_FILTER
filter for interaction log files
|
static javax.swing.filechooser.FileFilter |
JAVA_FILTER
filter for single java source files
|
static javax.swing.filechooser.FileFilter |
KEY_FILTER
file filter for *.key files
|
static javax.swing.filechooser.FileFilter |
PROOF_BUNDLE_FILTER
filter for proof bundles
|
static javax.swing.filechooser.FileFilter |
STATISTICS_FILTER
The Constant for the filter for statistics files.
|
static javax.swing.filechooser.FileFilter |
ZIP_FILTER
filter for zip archives
|
ACCEPT_ALL_FILE_FILTER_USED_CHANGED_PROPERTY, accessibleContext, ACCESSORY_CHANGED_PROPERTY, APPROVE_BUTTON_MNEMONIC_CHANGED_PROPERTY, APPROVE_BUTTON_TEXT_CHANGED_PROPERTY, APPROVE_BUTTON_TOOL_TIP_TEXT_CHANGED_PROPERTY, APPROVE_OPTION, APPROVE_SELECTION, CANCEL_OPTION, CANCEL_SELECTION, CHOOSABLE_FILE_FILTER_CHANGED_PROPERTY, CONTROL_BUTTONS_ARE_SHOWN_CHANGED_PROPERTY, CUSTOM_DIALOG, DIALOG_TITLE_CHANGED_PROPERTY, DIALOG_TYPE_CHANGED_PROPERTY, DIRECTORIES_ONLY, DIRECTORY_CHANGED_PROPERTY, ERROR_OPTION, FILE_FILTER_CHANGED_PROPERTY, FILE_HIDING_CHANGED_PROPERTY, FILE_SELECTION_MODE_CHANGED_PROPERTY, FILE_SYSTEM_VIEW_CHANGED_PROPERTY, FILE_VIEW_CHANGED_PROPERTY, FILES_AND_DIRECTORIES, FILES_ONLY, MULTI_SELECTION_ENABLED_CHANGED_PROPERTY, OPEN_DIALOG, SAVE_DIALOG, SELECTED_FILE_CHANGED_PROPERTY, SELECTED_FILES_CHANGED_PROPERTY
listenerList, TOOL_TIP_TEXT_KEY, ui, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW
Modifier and Type | Method and Description |
---|---|
void |
approveSelection() |
static KeYFileChooser |
getFileChooser(java.lang.String title)
Gets the file chooser for the prover.
|
void |
prepare() |
void |
setDialogTitle(java.lang.String title) |
int |
showOpenDialog(java.awt.Component component) |
int |
showSaveDialog(java.awt.Component parent) |
int |
showSaveDialog(java.awt.Component parent,
java.io.File selectedFile)
Shows the dialog with the given file/directory as currently selected.
|
int |
showSaveDialog(java.awt.Component parent,
java.io.File originalFile,
java.lang.String extension)
Show a file dialog for saving a file.
|
boolean |
useCompression() |
accept, addActionListener, addChoosableFileFilter, cancelSelection, changeToParentDirectory, createDialog, ensureFileIsVisible, fireActionPerformed, getAcceptAllFileFilter, getAccessibleContext, getAccessory, getActionListeners, getApproveButtonMnemonic, getApproveButtonText, getApproveButtonToolTipText, getChoosableFileFilters, getControlButtonsAreShown, getCurrentDirectory, getDescription, getDialogTitle, getDialogType, getDragEnabled, getFileFilter, getFileSelectionMode, getFileSystemView, getFileView, getIcon, getName, getSelectedFile, getSelectedFiles, getTypeDescription, getUI, getUIClassID, isAcceptAllFileFilterUsed, isDirectorySelectionEnabled, isFileHidingEnabled, isFileSelectionEnabled, isMultiSelectionEnabled, isTraversable, paramString, removeActionListener, removeChoosableFileFilter, rescanCurrentDirectory, resetChoosableFileFilters, setAcceptAllFileFilterUsed, setAccessory, setApproveButtonMnemonic, setApproveButtonMnemonic, setApproveButtonText, setApproveButtonToolTipText, setControlButtonsAreShown, setCurrentDirectory, setDialogType, setDragEnabled, setFileFilter, setFileHidingEnabled, setFileSelectionMode, setFileSystemView, setFileView, setMultiSelectionEnabled, setSelectedFile, setSelectedFiles, setup, showDialog, updateUI
addAncestorListener, addNotify, addVetoableChangeListener, computeVisibleRect, contains, createToolTip, disable, enable, firePropertyChange, firePropertyChange, firePropertyChange, fireVetoableChange, getActionForKeyStroke, getActionMap, getAlignmentX, getAlignmentY, getAncestorListeners, getAutoscrolls, getBaseline, getBaselineResizeBehavior, getBorder, getBounds, getClientProperty, getComponentGraphics, getComponentPopupMenu, getConditionForKeyStroke, getDebugGraphicsOptions, getDefaultLocale, getFontMetrics, getGraphics, getHeight, getInheritsPopupMenu, getInputMap, getInputMap, getInputVerifier, getInsets, getInsets, getListeners, getLocation, getMaximumSize, getMinimumSize, getNextFocusableComponent, getPopupLocation, getPreferredSize, getRegisteredKeyStrokes, getRootPane, getSize, getToolTipLocation, getToolTipText, getToolTipText, getTopLevelAncestor, getTransferHandler, getVerifyInputWhenFocusTarget, getVetoableChangeListeners, getVisibleRect, getWidth, getX, getY, grabFocus, hide, isDoubleBuffered, isLightweightComponent, isManagingFocus, isOpaque, isOptimizedDrawingEnabled, isPaintingForPrint, isPaintingOrigin, isPaintingTile, isRequestFocusEnabled, isValidateRoot, paint, paintBorder, paintChildren, paintComponent, paintImmediately, paintImmediately, print, printAll, printBorder, printChildren, printComponent, processComponentKeyEvent, processKeyBinding, processKeyEvent, processMouseEvent, processMouseMotionEvent, putClientProperty, registerKeyboardAction, registerKeyboardAction, removeAncestorListener, removeNotify, removeVetoableChangeListener, repaint, repaint, requestDefaultFocus, requestFocus, requestFocus, requestFocusInWindow, requestFocusInWindow, resetKeyboardActions, reshape, revalidate, scrollRectToVisible, setActionMap, setAlignmentX, setAlignmentY, setAutoscrolls, setBackground, setBorder, setComponentPopupMenu, setDebugGraphicsOptions, setDefaultLocale, setDoubleBuffered, setEnabled, setFocusTraversalKeys, setFont, setForeground, setInheritsPopupMenu, setInputMap, setInputVerifier, setMaximumSize, setMinimumSize, setNextFocusableComponent, setOpaque, setPreferredSize, setRequestFocusEnabled, setToolTipText, setTransferHandler, setUI, setVerifyInputWhenFocusTarget, setVisible, unregisterKeyboardAction, update
add, add, add, add, add, addContainerListener, addImpl, addPropertyChangeListener, addPropertyChangeListener, applyComponentOrientation, areFocusTraversalKeysSet, countComponents, deliverEvent, doLayout, findComponentAt, findComponentAt, getComponent, getComponentAt, getComponentAt, getComponentCount, getComponents, getComponentZOrder, getContainerListeners, getFocusTraversalKeys, getFocusTraversalPolicy, getLayout, getMousePosition, insets, invalidate, isAncestorOf, isFocusCycleRoot, isFocusCycleRoot, isFocusTraversalPolicyProvider, isFocusTraversalPolicySet, layout, list, list, locate, minimumSize, paintComponents, preferredSize, printComponents, processContainerEvent, processEvent, remove, remove, removeAll, removeContainerListener, setComponentZOrder, setFocusCycleRoot, setFocusTraversalPolicy, setFocusTraversalPolicyProvider, setLayout, transferFocusDownCycle, validate, validateTree
action, add, addComponentListener, addFocusListener, addHierarchyBoundsListener, addHierarchyListener, addInputMethodListener, addKeyListener, addMouseListener, addMouseMotionListener, addMouseWheelListener, bounds, checkImage, checkImage, coalesceEvents, contains, createImage, createImage, createVolatileImage, createVolatileImage, disableEvents, dispatchEvent, enable, enableEvents, enableInputMethods, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, getBackground, getBounds, getColorModel, getComponentListeners, getComponentOrientation, getCursor, getDropTarget, getFocusCycleRootAncestor, getFocusListeners, getFocusTraversalKeysEnabled, getFont, getForeground, getGraphicsConfiguration, getHierarchyBoundsListeners, getHierarchyListeners, getIgnoreRepaint, getInputContext, getInputMethodListeners, getInputMethodRequests, getKeyListeners, getLocale, getLocation, getLocationOnScreen, getMouseListeners, getMouseMotionListeners, getMousePosition, getMouseWheelListeners, getName, getParent, getPeer, getPropertyChangeListeners, getPropertyChangeListeners, getSize, getToolkit, getTreeLock, gotFocus, handleEvent, hasFocus, imageUpdate, inside, isBackgroundSet, isCursorSet, isDisplayable, isEnabled, isFocusable, isFocusOwner, isFocusTraversable, isFontSet, isForegroundSet, isLightweight, isMaximumSizeSet, isMinimumSizeSet, isPreferredSizeSet, isShowing, isValid, isVisible, keyDown, keyUp, list, list, list, location, lostFocus, mouseDown, mouseDrag, mouseEnter, mouseExit, mouseMove, mouseUp, move, nextFocus, paintAll, postEvent, prepareImage, prepareImage, processComponentEvent, processFocusEvent, processHierarchyBoundsEvent, processHierarchyEvent, processInputMethodEvent, processMouseWheelEvent, remove, removeComponentListener, removeFocusListener, removeHierarchyBoundsListener, removeHierarchyListener, removeInputMethodListener, removeKeyListener, removeMouseListener, removeMouseMotionListener, removeMouseWheelListener, removePropertyChangeListener, removePropertyChangeListener, repaint, repaint, repaint, resize, resize, setBounds, setBounds, setComponentOrientation, setCursor, setDropTarget, setFocusable, setFocusTraversalKeysEnabled, setIgnoreRepaint, setLocale, setLocation, setLocation, setName, setSize, setSize, show, show, size, toString, transferFocus, transferFocusBackward, transferFocusUpCycle
public static final javax.swing.filechooser.FileFilter DEFAULT_FILTER
public static final javax.swing.filechooser.FileFilter KEY_FILTER
public static final javax.swing.filechooser.FileFilter STATISTICS_FILTER
public static final javax.swing.filechooser.FileFilter JAVA_FILTER
public static final javax.swing.filechooser.FileFilter COMPRESSED_FILTER
public static final javax.swing.filechooser.FileFilter INTERACTION_LOG_FILTER
public static final javax.swing.filechooser.FileFilter ZIP_FILTER
public static final javax.swing.filechooser.FileFilter PROOF_BUNDLE_FILTER
public boolean useCompression()
public void approveSelection()
approveSelection
in class javax.swing.JFileChooser
public void prepare()
public void setDialogTitle(java.lang.String title)
setDialogTitle
in class javax.swing.JFileChooser
public int showSaveDialog(java.awt.Component parent)
showSaveDialog
in class javax.swing.JFileChooser
public int showSaveDialog(java.awt.Component parent, java.io.File originalFile, java.lang.String extension)
parent
- the main windoworiginalFile
- the original file to be saved, if it exists and is a proof, this will be the suggestionextension
- the desired file name extension (usually ".proof")JFileChooser.APPROVE_OPTION
, JFileChooser.CANCEL_OPTION
, or JFileChooser.ERROR_OPTION
public int showSaveDialog(java.awt.Component parent, java.io.File selectedFile)
parent
- the Component the dialog is overselectedFile
- the file or directory that shall be currently selectedJFileChooser.APPROVE_OPTION
, JFileChooser.CANCEL_OPTION
, or JFileChooser.ERROR_OPTION
public int showOpenDialog(java.awt.Component component)
showOpenDialog
in class javax.swing.JFileChooser
public static KeYFileChooser getFileChooser(java.lang.String title)
title
- the title of the key file chooserCopyright © 2003-2019 The KeY-Project.