1036 |
"PAGE_UP", "scrollUpChangeSelection", |
"PAGE_UP", "scrollUpChangeSelection", |
1037 |
"ctrl PAGE_DOWN", "scrollDownChangeLead" |
"ctrl PAGE_DOWN", "scrollDownChangeLead" |
1038 |
}), |
}), |
1039 |
"Tree.font", new FontUIResource("Dialog", Font.PLAIN, 12), |
"Tree.font", new FontUIResource(new Font("Helvetica", Font.PLAIN, 12)), |
1040 |
"Tree.foreground", new ColorUIResource(Color.black), |
"Tree.foreground", new ColorUIResource(Color.black), |
1041 |
"Tree.hash", new ColorUIResource(Color.gray), |
"Tree.hash", new ColorUIResource(Color.gray), |
1042 |
"Tree.leftChildIndent", new Integer(7), |
"Tree.leftChildIndent", new Integer(7), |