public class SequentHideWarningBorder
extends javax.swing.border.TitledBorder
SequentView.isHiding()
,
Serialized FormABOVE_BOTTOM, ABOVE_TOP, BELOW_BOTTOM, BELOW_TOP, border, BOTTOM, CENTER, DEFAULT_JUSTIFICATION, DEFAULT_POSITION, EDGE_SPACING, LEADING, LEFT, RIGHT, TEXT_INSET_H, TEXT_SPACING, title, titleColor, titleFont, titleJustification, titlePosition, TOP, TRAILING
Constructor and Description |
---|
SequentHideWarningBorder(java.lang.String title,
SequentView sequentView)
Instantiates a new sequent border.
|
Modifier and Type | Method and Description |
---|---|
void |
paintBorder(java.awt.Component c,
java.awt.Graphics g,
int x,
int y,
int width,
int height) |
getBaseline, getBaselineResizeBehavior, getBorder, getBorderInsets, getFont, getMinimumSize, getTitle, getTitleColor, getTitleFont, getTitleJustification, getTitlePosition, isBorderOpaque, setBorder, setTitle, setTitleColor, setTitleFont, setTitleJustification, setTitlePosition
public SequentHideWarningBorder(java.lang.String title, SequentView sequentView)
title
- the title to displaysequentView
- the sequent view which will be wrapped by the componentCopyright © 2003-2019 The KeY-Project.