public class InteractionLogView extends javax.swing.JPanel implements InteractionRecorderListener, TabPanel
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(MainWindow window,
KeYMediator mediator) |
Modifier and Type | Method and Description |
---|---|
org.key_project.ui.interactionlog.InteractionLogView.AddUserNoteAction |
getActionAddUserNote() |
org.key_project.ui.interactionlog.InteractionLogView.ExportMarkdownAction |
getActionExportMarkdown() |
org.key_project.ui.interactionlog.InteractionLogView.ExportMUScriptAction |
getActionExportProofScript() |
org.key_project.ui.interactionlog.InteractionLogView.JumpIntoTreeAction |
getActionJumpIntoTree() |
org.key_project.ui.interactionlog.InteractionLogView.ExportKPSAction |
getActionKPSExport() |
org.key_project.ui.interactionlog.InteractionLogView.LoadAction |
getActionLoad() |
org.key_project.ui.interactionlog.InteractionLogView.ExportMUScriptClipboardAction |
getActionMUCopyClipboard() |
org.key_project.ui.interactionlog.InteractionLogView.PauseLoggingAction |
getActionPauseLogging() |
org.key_project.ui.interactionlog.InteractionLogView.SaveAction |
getActionSave() |
org.key_project.ui.interactionlog.InteractionLogView.ShowExtendedActionsAction |
getActionShowExtended() |
org.key_project.ui.interactionlog.InteractionLogView.ToggleFavouriteAction |
getActionToggleFavourite() |
org.key_project.ui.interactionlog.InteractionLogView.TryReapplyAction |
getActionTryReapply() |
javax.swing.JComponent |
getComponent() |
javax.swing.Icon |
getIcon() |
javax.swing.DefaultListModel<Interaction> |
getInteractionListModel() |
javax.swing.JComboBox<InteractionLog> |
getInteractionLogSelection() |
javax.swing.JList<Interaction> |
getListInteraction() |
InteractionRecorder |
getRecorder() |
java.lang.String |
getTitle() |
void |
onInteraction(Interaction interaction) |
void |
setMainWindow(MainWindow window) |
void |
setMediator(KeYMediator mediator) |
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
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getPermissions, getTitleActions, getTitleCActions
public InteractionLogView(MainWindow window, KeYMediator mediator)
public void onInteraction(Interaction interaction)
onInteraction
in interface InteractionRecorderListener
public org.key_project.ui.interactionlog.InteractionLogView.ExportMUScriptAction getActionExportProofScript()
public org.key_project.ui.interactionlog.InteractionLogView.SaveAction getActionSave()
public org.key_project.ui.interactionlog.InteractionLogView.LoadAction getActionLoad()
public org.key_project.ui.interactionlog.InteractionLogView.AddUserNoteAction getActionAddUserNote()
public org.key_project.ui.interactionlog.InteractionLogView.JumpIntoTreeAction getActionJumpIntoTree()
public org.key_project.ui.interactionlog.InteractionLogView.TryReapplyAction getActionTryReapply()
public InteractionRecorder getRecorder()
public void setMediator(KeYMediator mediator)
public void setMainWindow(MainWindow window)
public org.key_project.ui.interactionlog.InteractionLogView.ExportKPSAction getActionKPSExport()
public org.key_project.ui.interactionlog.InteractionLogView.ToggleFavouriteAction getActionToggleFavourite()
public org.key_project.ui.interactionlog.InteractionLogView.ExportMarkdownAction getActionExportMarkdown()
public org.key_project.ui.interactionlog.InteractionLogView.ShowExtendedActionsAction getActionShowExtended()
public org.key_project.ui.interactionlog.InteractionLogView.ExportMUScriptClipboardAction getActionMUCopyClipboard()
public org.key_project.ui.interactionlog.InteractionLogView.PauseLoggingAction getActionPauseLogging()
public javax.swing.JList<Interaction> getListInteraction()
public javax.swing.JComboBox<InteractionLog> getInteractionLogSelection()
public javax.swing.DefaultListModel<Interaction> getInteractionListModel()
public javax.swing.JComponent getComponent()
getComponent
in interface TabPanel
Copyright © 2003-2019 The KeY-Project.