org.grinvin.grinvin
Class GrinvinWindow
JFrame
org.grinvin.grinvin.GrinvinWindow
public class GrinvinWindow
extends JFrame
This class represents the GrInvIn main window.
GrinvinWindow
public GrinvinWindow()
Creates a new instance of GrinvinWindow
addTabsChangeListener
public void addTabsChangeListener(ChangeListener l)
getGraphListsListSelectionModel
public ListSelectionModel getGraphListsListSelectionModel()
getSelectedTab
public String getSelectedTab()
getWindow
public Window getWindow(String key)
Retrieve the application window with the given key. Current
available keys are
- AvailableInvariantsList for the invariant tree window
- EditorWindow for the graph editor
- FactoryWindow for the list of graph factories
- ConjecturingWindow for the conjecturing window
loadGraphListWindowsInMenu
public void loadGraphListWindowsInMenu()
Install the menu for the graphs lists window and its associated
window group.
removeTabsChangeListener
public void removeTabsChangeListener(ChangeListener l)
setSelectedTab
public void setSelectedTab(String key)
setWindow
public void setWindow(String key,
Window window)
Set the application window for the given key. See
getWindow(String)
for possible keys. Also installs a menu command which enables the
window to be made visible.