public class ShowHashcodesExtension extends java.lang.Object implements KeYGuiExtension, KeYGuiExtension.Tooltip
KeYGuiExtension.ContextMenu, KeYGuiExtension.Info, KeYGuiExtension.KeyboardShortcuts, KeYGuiExtension.LeftPanel, KeYGuiExtension.MainMenu, KeYGuiExtension.Settings, KeYGuiExtension.Startup, KeYGuiExtension.StatusLine, KeYGuiExtension.TermInfo, KeYGuiExtension.Toolbar, KeYGuiExtension.Tooltip
Constructor and Description |
---|
ShowHashcodesExtension() |
Modifier and Type | Method and Description |
---|---|
java.util.List<java.lang.String> |
getTooltipStrings(MainWindow mainWindow,
PosInSequent pos) |
public java.util.List<java.lang.String> getTooltipStrings(MainWindow mainWindow, PosInSequent pos)
getTooltipStrings
in interface KeYGuiExtension.Tooltip
mainWindow
- the main window.pos
- the position of the term whose info shall be shown.Copyright © 2003-2019 The KeY-Project.