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