1041 |
"Tree.hash", new ColorUIResource(Color.gray), |
"Tree.hash", new ColorUIResource(Color.gray), |
1042 |
"Tree.leftChildIndent", new Integer(7), |
"Tree.leftChildIndent", new Integer(7), |
1043 |
"Tree.rightChildIndent", new Integer(13), |
"Tree.rightChildIndent", new Integer(13), |
1044 |
"Tree.rowHeight", new Integer(19), |
"Tree.rowHeight", new Integer(20), // FIXME |
1045 |
"Tree.scrollsOnExpand", Boolean.TRUE, |
"Tree.scrollsOnExpand", Boolean.TRUE, |
1046 |
"Tree.selectionBackground", new ColorUIResource(Color.black), |
"Tree.selectionBackground", new ColorUIResource(Color.black), |
1047 |
"Tree.nonSelectionBackground", new ColorUIResource(light), |
"Tree.nonSelectionBackground", new ColorUIResource(light), |