public class InteractionLogView extends javax.swing.JPanel implements InteractionRecorderListener
Modifier and Type | Class and Description |
---|---|
private class |
InteractionLogView.AbstractFileSaveAction |
private class |
InteractionLogView.AddUserNoteAction |
private class |
InteractionLogView.ExportKPSAction |
private class |
InteractionLogView.ExportMarkdownAction |
private class |
InteractionLogView.ExportMUScriptAction |
private class |
InteractionLogView.ExportMUScriptClipboardAction |
private class |
InteractionLogView.JumpIntoTreeAction |
private class |
InteractionLogView.LoadAction |
private class |
InteractionLogView.PauseLoggingAction |
private class |
InteractionLogView.SaveAction |
private class |
InteractionLogView.ShowExtendedActionsAction |
private class |
InteractionLogView.ToggleFavouriteAction |
private class |
InteractionLogView.TryReapplyAction |
javax.swing.JPanel.AccessibleJPanel
javax.swing.JComponent.AccessibleJComponent
listenerList, TOOL_TIP_TEXT_KEY, ui, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW
Constructor and Description |
---|
InteractionLogView() |
getAccessibleContext, getUI, getUIClassID, paramString, setUI, 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
private static final long serialVersionUID
private static final float SMALL_ICON_SIZE
private static final java.lang.String MENU_ILOG
private static final java.lang.String MENU_ILOG_EXPORT
private final InteractionRecorder recorder
private final InteractionLogView.ExportMUScriptAction actionExportProofScript
private final InteractionLogView.ExportKPSAction actionKPSExport
private final InteractionLogView.SaveAction actionSave
private final InteractionLogView.LoadAction actionLoad
private final InteractionLogView.AddUserNoteAction actionAddUserNote
private final InteractionLogView.ToggleFavouriteAction actionToggleFavourite
private final InteractionLogView.JumpIntoTreeAction actionJumpIntoTree
private final InteractionLogView.TryReapplyAction actionTryReapply
private final InteractionLogView.ExportMarkdownAction actionExportMarkdown
private final InteractionLogView.ShowExtendedActionsAction actionShowExtended
private final InteractionLogView.ExportMUScriptClipboardAction actionMUCopyClipboard
private final InteractionLogView.PauseLoggingAction actionPauseLogging
private final javax.swing.JList<Interaction> listInteraction
private final javax.swing.JComboBox<InteractionLog> interactionLogSelection
private final javax.swing.DefaultListModel<Interaction> interactionListModel
private KeYMediator mediator
private Proof currentProof
private final KeYSelectionListener keYSelectionListener
private javax.swing.JFileChooser fileChooser
private void handleSelectionChange(java.awt.event.ActionEvent actionEvent)
private InteractionLog getSelectedItem()
private void setCurrentProof(Proof proof)
private void rebuildList()
private void updateList(InteractionLog interactionLog)
private javax.swing.JFileChooser getFileChooser()
public void onInteraction(Interaction interaction)
onInteraction
in interface InteractionRecorderListener
public InteractionLogView.ExportMUScriptAction getActionExportProofScript()
public InteractionLogView.SaveAction getActionSave()
public InteractionLogView.LoadAction getActionLoad()
public InteractionLogView.AddUserNoteAction getActionAddUserNote()
public InteractionLogView.JumpIntoTreeAction getActionJumpIntoTree()
public InteractionLogView.TryReapplyAction getActionTryReapply()
public InteractionRecorder getRecorder()
public void setMediator(KeYMediator mediator)
public void setMainWindow(MainWindow window)
public InteractionLogView.ExportKPSAction getActionKPSExport()
public InteractionLogView.ToggleFavouriteAction getActionToggleFavourite()
public InteractionLogView.ExportMarkdownAction getActionExportMarkdown()
public InteractionLogView.ShowExtendedActionsAction getActionShowExtended()
public InteractionLogView.ExportMUScriptClipboardAction getActionMUCopyClipboard()
public InteractionLogView.PauseLoggingAction getActionPauseLogging()
public javax.swing.JList<Interaction> getListInteraction()
public javax.swing.JComboBox<InteractionLog> getInteractionLogSelection()
public javax.swing.DefaultListModel<Interaction> getInteractionListModel()