public final class GuiUtilities extends Object
Modifier | Constructor and Description |
---|---|
private |
GuiUtilities() |
Modifier and Type | Method and Description |
---|---|
static void |
copyHighlightToClipboard(CurrentGoalView view,
PosInSequent pos) |
static void |
paintEmptyViewComponent(JComponent pane,
String name)
paints empty view with white background.
|
static void |
setCenter(Component comp)
Center a component on the screen.
|
static void |
setCenter(Component comp,
Component parent)
Center a component within a parental component.
|
public static void paintEmptyViewComponent(JComponent pane, String name)
public static void copyHighlightToClipboard(CurrentGoalView view, PosInSequent pos)
public static void setCenter(Component comp)
comp
- the component to be centered relative to the screen. It must
already have its final size set.setCenter(Component, Component)
public static void setCenter(Component comp, Component parent)
comp
- the component to be centered.parent
- center relative to what. null
to center relative
to screen.setCenter(Component)