744 |
return c; |
return c; |
745 |
} |
} |
746 |
|
|
747 |
public static JRadioButton mkRadio(String label) |
public static JPanel mkRadio(String label) |
748 |
{ |
{ |
749 |
|
JPanel p = new JPanel(); |
750 |
JRadioButton c = new JRadioButton(label); |
JRadioButton c = new JRadioButton(label); |
751 |
c.setFont(new Font("Luxi", Font.PLAIN, 14)); |
JRadioButton d = new JRadioButton("not " + label); |
752 |
return c; |
ButtonGroup bg = new ButtonGroup(); |
753 |
|
bg.add(c); |
754 |
|
bg.add(d); |
755 |
|
p.add(c); |
756 |
|
p.add(d); |
757 |
|
return p; |
758 |
} |
} |
759 |
|
|
760 |
public static JList mkList(Object[] elts) |
public static JList mkList(Object[] elts) |