public class TacletTranslationSelection extends Object
Modifier and Type | Field and Description |
---|---|
private DefaultTreeCellRenderer |
cellRenderer |
private static int |
EDIT |
private static int |
INNER_PANEL |
private static int |
LEAF_PANEL |
private static int |
PAINT |
private JTree |
selectionTree |
private SMTSettings |
smtSettings |
private TreePanel[][] |
treePanels |
Constructor and Description |
---|
TacletTranslationSelection(SMTSettings smtSettings) |
Modifier and Type | Method and Description |
---|---|
private int |
getItemHeight(TreeModel model) |
static KeYSelectionListener |
getSelectionListener() |
JTree |
getSelectionTree() |
private TreeCellEditor |
getTreeCellEditor() |
private DefaultTreeCellRenderer |
getTreeCellRenderer() |
protected SupportedTaclets.TreeItem |
treeItem(TreeNode node) |
private DefaultTreeCellRenderer cellRenderer
private JTree selectionTree
private static final int INNER_PANEL
private static final int LEAF_PANEL
private static final int PAINT
private static final int EDIT
private TreePanel[][] treePanels
private final SMTSettings smtSettings
public TacletTranslationSelection(SMTSettings smtSettings)
public static KeYSelectionListener getSelectionListener()
protected SupportedTaclets.TreeItem treeItem(TreeNode node)
private int getItemHeight(TreeModel model)
public JTree getSelectionTree()
private TreeCellEditor getTreeCellEditor()
private DefaultTreeCellRenderer getTreeCellRenderer()