public class MergePartnerSelectionDialog
extends javax.swing.JDialog
MergeRule
application.javax.swing.JDialog.AccessibleJDialog
java.awt.Dialog.AccessibleAWTDialog, java.awt.Dialog.ModalExclusionType, java.awt.Dialog.ModalityType
java.awt.Window.AccessibleAWTWindow, java.awt.Window.Type
Modifier and Type | Field and Description |
---|---|
private javax.swing.ButtonGroup |
bgMergeMethods |
private java.util.LinkedList<MergePartner> |
candidates |
private static java.lang.String |
CB_SELECT_CANDIDATE_HINT
The tooltip hint for the checkbox.
|
private javax.swing.JCheckBox |
cbSelectCandidate |
private static java.lang.String |
CHOOSE_ALL_BTN_TOOLTIP_TXT
The tooltip for the OK button
|
private javax.swing.JButton |
chooseAllButton |
private Term |
chosenDistForm
The chosen distinguishing formula
|
private java.util.SortedSet<MergePartner> |
chosenGoals
The chosen goals.
|
private MergeProcedure |
chosenRule
The chosen merge method.
|
private javax.swing.JComboBox<java.lang.String> |
cmbCandidates |
private static java.util.Comparator<MergePartner> |
GOAL_COMPARATOR
Comparator for goals; sorts by serial nr. of the node
|
private static java.awt.Dimension |
INITIAL_SIZE
The initial size of this dialog.
|
private static MainWindow |
MAIN_WINDOW_INSTANCE |
private Pair<Goal,PosInOccurrence> |
mergeGoalPio |
private static java.lang.String |
OK_BTN_TOOLTIP_TXT
The tooltip for the choose-all button
|
private javax.swing.JButton |
okButton |
private javax.swing.JScrollPane |
scrpPartner1 |
private javax.swing.JScrollPane |
scrpPartner2 |
private static long |
serialVersionUID |
private Services |
services |
private static java.awt.Font |
TXT_AREA_FONT
The font for the JEditorPanes.
|
private javax.swing.JTextField |
txtDistForm |
private javax.swing.JEditorPane |
txtPartner1 |
private javax.swing.JEditorPane |
txtPartner2 |
accessibleContext, rootPane, rootPaneCheckingEnabled
BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT
Modifier | Constructor and Description |
---|---|
private |
MergePartnerSelectionDialog() |
|
MergePartnerSelectionDialog(Goal mergeGoal,
PosInOccurrence pio,
ImmutableList<MergePartner> candidates,
Services services)
Creates a new merge partner selection dialog.
|
Modifier and Type | Method and Description |
---|---|
private void |
checkApplicable()
Enables / disables the OK and Choose all button depending on whether or
not the currently chosen merge rule instance is applicable.
|
private static boolean |
checkProvability(Sequent seq,
Term formulaToProve,
Services services)
Checks whether the given formula can be proven within the given sequent.
|
ImmutableList<MergePartner> |
getChosenCandidates() |
Term |
getChosenDistinguishingFormula() |
<T extends MergeProcedure> |
getChosenMergeRule() |
private MergePartner |
getNthCandidate(int n)
Returns the n-th candidate in the list.
|
private MergePartner |
getSelectedCandidate() |
private <T> ImmutableList<T> |
immutableListFromIterabe(java.lang.Iterable<T> it) |
private boolean |
isApplicableForCandidates(ImmutableList<MergePartner> theCandidates)
Checks whether the merge rule is applicable for the given set of
candidates.
|
private boolean |
isSuitableDistFormula()
Checks whether the selected distinguishable formula is actually suitable
for this purpose.
|
private void |
loadCandidates()
Loads the merge candidates into the combo box, initializes the partner
editor pane with the text of the first candidate.
|
private void |
setHighlightedSequentForArea(Goal goal,
PosInOccurrence pio,
javax.swing.JEditorPane area)
Adds the given goal to the given editor pane, with the portion that
corresponds to the given position highlighted in bold.
|
addImpl, createRootPane, dialogInit, getAccessibleContext, getContentPane, getDefaultCloseOperation, getGlassPane, getGraphics, getJMenuBar, getLayeredPane, getRootPane, getTransferHandler, isDefaultLookAndFeelDecorated, isRootPaneCheckingEnabled, paramString, processWindowEvent, remove, repaint, setContentPane, setDefaultCloseOperation, setDefaultLookAndFeelDecorated, setGlassPane, setJMenuBar, setLayeredPane, setLayout, setRootPane, setRootPaneCheckingEnabled, setTransferHandler, update
addNotify, getModalityType, getTitle, hide, isModal, isResizable, isUndecorated, setBackground, setModal, setModalityType, setOpacity, setResizable, setShape, setTitle, setUndecorated, setVisible, show, toBack
addPropertyChangeListener, addPropertyChangeListener, addWindowFocusListener, addWindowListener, addWindowStateListener, applyResourceBundle, applyResourceBundle, createBufferStrategy, createBufferStrategy, dispose, getBackground, getBufferStrategy, getFocusableWindowState, getFocusCycleRootAncestor, getFocusOwner, getFocusTraversalKeys, getIconImages, getInputContext, getListeners, getLocale, getModalExclusionType, getMostRecentFocusOwner, getOpacity, getOwnedWindows, getOwner, getOwnerlessWindows, getShape, getToolkit, getType, getWarningString, getWindowFocusListeners, getWindowListeners, getWindows, getWindowStateListeners, isActive, isAlwaysOnTop, isAlwaysOnTopSupported, isAutoRequestFocus, isFocusableWindow, isFocusCycleRoot, isFocused, isLocationByPlatform, isOpaque, isShowing, isValidateRoot, pack, paint, postEvent, processEvent, processWindowFocusEvent, processWindowStateEvent, removeNotify, removeWindowFocusListener, removeWindowListener, removeWindowStateListener, reshape, setAlwaysOnTop, setAutoRequestFocus, setBounds, setBounds, setCursor, setFocusableWindowState, setFocusCycleRoot, setIconImage, setIconImages, setLocation, setLocation, setLocationByPlatform, setLocationRelativeTo, setMinimumSize, setModalExclusionType, setSize, setSize, setType, toFront
add, add, add, add, add, addContainerListener, applyComponentOrientation, areFocusTraversalKeysSet, countComponents, deliverEvent, doLayout, findComponentAt, findComponentAt, getAlignmentX, getAlignmentY, getComponent, getComponentAt, getComponentAt, getComponentCount, getComponents, getComponentZOrder, getContainerListeners, getFocusTraversalPolicy, getInsets, getLayout, getMaximumSize, getMinimumSize, getMousePosition, getPreferredSize, insets, invalidate, isAncestorOf, isFocusCycleRoot, isFocusTraversalPolicyProvider, isFocusTraversalPolicySet, layout, list, list, locate, minimumSize, paintComponents, preferredSize, print, printComponents, processContainerEvent, remove, removeAll, removeContainerListener, setComponentZOrder, setFocusTraversalKeys, setFocusTraversalPolicy, setFocusTraversalPolicyProvider, setFont, transferFocusDownCycle, validate, validateTree
action, add, addComponentListener, addFocusListener, addHierarchyBoundsListener, addHierarchyListener, addInputMethodListener, addKeyListener, addMouseListener, addMouseMotionListener, addMouseWheelListener, bounds, checkImage, checkImage, coalesceEvents, contains, contains, createImage, createImage, createVolatileImage, createVolatileImage, disable, disableEvents, dispatchEvent, enable, enable, enableEvents, enableInputMethods, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, getBaseline, getBaselineResizeBehavior, getBounds, getBounds, getColorModel, getComponentListeners, getComponentOrientation, getCursor, getDropTarget, getFocusListeners, getFocusTraversalKeysEnabled, getFont, getFontMetrics, getForeground, getGraphicsConfiguration, getHeight, getHierarchyBoundsListeners, getHierarchyListeners, getIgnoreRepaint, getInputMethodListeners, getInputMethodRequests, getKeyListeners, getLocation, getLocation, getLocationOnScreen, getMouseListeners, getMouseMotionListeners, getMousePosition, getMouseWheelListeners, getName, getParent, getPeer, getPropertyChangeListeners, getPropertyChangeListeners, getSize, getSize, getTreeLock, getWidth, getX, getY, gotFocus, handleEvent, hasFocus, imageUpdate, inside, isBackgroundSet, isCursorSet, isDisplayable, isDoubleBuffered, isEnabled, isFocusable, isFocusOwner, isFocusTraversable, isFontSet, isForegroundSet, isLightweight, isMaximumSizeSet, isMinimumSizeSet, isPreferredSizeSet, isValid, isVisible, keyDown, keyUp, list, list, list, location, lostFocus, mouseDown, mouseDrag, mouseEnter, mouseExit, mouseMove, mouseUp, move, nextFocus, paintAll, prepareImage, prepareImage, printAll, processComponentEvent, processFocusEvent, processHierarchyBoundsEvent, processHierarchyEvent, processInputMethodEvent, processKeyEvent, processMouseEvent, processMouseMotionEvent, processMouseWheelEvent, remove, removeComponentListener, removeFocusListener, removeHierarchyBoundsListener, removeHierarchyListener, removeInputMethodListener, removeKeyListener, removeMouseListener, removeMouseMotionListener, removeMouseWheelListener, removePropertyChangeListener, removePropertyChangeListener, repaint, repaint, repaint, requestFocus, requestFocus, requestFocusInWindow, requestFocusInWindow, resize, resize, revalidate, setComponentOrientation, setDropTarget, setEnabled, setFocusable, setFocusTraversalKeysEnabled, setForeground, setIgnoreRepaint, setLocale, setMaximumSize, setName, setPreferredSize, show, size, toString, transferFocus, transferFocusBackward, transferFocusUpCycle
private static final long serialVersionUID
private static final java.lang.String CB_SELECT_CANDIDATE_HINT
private static final java.lang.String CHOOSE_ALL_BTN_TOOLTIP_TXT
private static final java.lang.String OK_BTN_TOOLTIP_TXT
private static final java.awt.Dimension INITIAL_SIZE
private static final java.awt.Font TXT_AREA_FONT
private static final MainWindow MAIN_WINDOW_INSTANCE
private static java.util.Comparator<MergePartner> GOAL_COMPARATOR
private java.util.LinkedList<MergePartner> candidates
private Services services
private Pair<Goal,PosInOccurrence> mergeGoalPio
private java.util.SortedSet<MergePartner> chosenGoals
private MergeProcedure chosenRule
private Term chosenDistForm
private javax.swing.JEditorPane txtPartner1
private javax.swing.JEditorPane txtPartner2
private javax.swing.JComboBox<java.lang.String> cmbCandidates
private javax.swing.JCheckBox cbSelectCandidate
private javax.swing.ButtonGroup bgMergeMethods
private final javax.swing.JTextField txtDistForm
private javax.swing.JScrollPane scrpPartner1
private javax.swing.JScrollPane scrpPartner2
private javax.swing.JButton okButton
private javax.swing.JButton chooseAllButton
private MergePartnerSelectionDialog()
public MergePartnerSelectionDialog(Goal mergeGoal, PosInOccurrence pio, ImmutableList<MergePartner> candidates, Services services)
mergeGoal
- The first (already chosen) merge partner.pio
- Position of Update-Modality-Postcondition formula in the
mergeNode.candidates
- Potential merge candidates.services
- The services object.public ImmutableList<MergePartner> getChosenCandidates()
public <T extends MergeProcedure> T getChosenMergeRule()
T
- public Term getChosenDistinguishingFormula()
private boolean isApplicableForCandidates(ImmutableList<MergePartner> theCandidates)
theCandidates
- Candidates to instantiate the merge rule application with.private void checkApplicable()
private boolean isSuitableDistFormula()
private static boolean checkProvability(Sequent seq, Term formulaToProve, Services services)
seq
- Sequent in which to check the provability of formulaToProve.formulaToProve
- Formula to prove.private <T> ImmutableList<T> immutableListFromIterabe(java.lang.Iterable<T> it)
it
- Iterable to convert into an ImmutableList.private MergePartner getSelectedCandidate()
private MergePartner getNthCandidate(int n)
n
- Index of the merge candidate.private void loadCandidates()
private void setHighlightedSequentForArea(Goal goal, PosInOccurrence pio, javax.swing.JEditorPane area)
goal
- Goal to add.pio
- Position indicating subterm to highlight.area
- The editor pane to add the highlighted goal to.