public final class GuiUtilities
extends java.lang.Object
Modifier | Constructor and Description |
---|---|
private |
GuiUtilities() |
Modifier and Type | Method and Description |
---|---|
static void |
copyHighlightToClipboard(CurrentGoalView view,
PosInSequent pos) |
static void |
paintEmptyViewComponent(javax.swing.JComponent pane,
java.lang.String name)
paints empty view with white background.
|
static void |
setCenter(java.awt.Component comp)
Center a component on the screen.
|
static void |
setCenter(java.awt.Component comp,
java.awt.Component parent)
Center a component within a parental component.
|
public static void paintEmptyViewComponent(javax.swing.JComponent pane, java.lang.String name)
public static void copyHighlightToClipboard(CurrentGoalView view, PosInSequent pos)
public static void setCenter(java.awt.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(java.awt.Component comp, java.awt.Component parent)
comp
- the component to be centered.parent
- center relative to what. null
to center relative
to screen.setCenter(Component)