ide
Class VeriSimDocumentFrame.NumberedBorder

java.lang.Object
  |
  +--javax.swing.border.AbstractBorder
        |
        +--javax.swing.border.EmptyBorder
              |
              +--ide.VeriSimDocumentFrame.NumberedBorder

class VeriSimDocumentFrame.NumberedBorder

extends javax.swing.border.EmptyBorder

Displays line numbers on the left of editor todo -> must be a inner class of Project and alocated only once.

See Also:

Serialized Form

Field Summary

int	bulletPosition
(package private) int	endHeight
(package private) int	fontHeight
(package private) int	left
(package private) int	startHeight
(package private) javax.swing.JViewport	vport

Fields inherited from class javax.swing.border.EmptyBorder

bottom, left, right, top

Constructor Summary

VeriSimDocumentFrame.NumberedBorder(int left, javax.swing.JViewport vport, int fontHeight)

Method Summary

void	paintBorder(java.awt.Component c, java.awt.Graphics g, int x, int y, int width, int height)
(package private) void	setFontHeight(int newH)

Methods inherited from class javax.swing.border.EmptyBorder

getBorderInsets, getBorderInsets, isBorderOpaque

Methods inherited from class javax.swing.border.AbstractBorder

getInteriorRectangle, getInteriorRectangle

Methods inherited from class java.lang.Object

, clone, equals, finalize, getClass, hashCode, notify, notifyAll, registerNatives, toString, wait, wait, wait

Field Detail

fontHeight

int fontHeight

startHeight

int startHeight

left

int left

endHeight

int endHeight

vport

javax.swing.JViewport vport

bulletPosition

public int bulletPosition

Constructor Detail

VeriSimDocumentFrame.NumberedBorder

public VeriSimDocumentFrame.NumberedBorder(int left,
                                           javax.swing.JViewport vport,
                                           int fontHeight)

Method Detail

paintBorder

public void paintBorder(java.awt.Component c,
                        java.awt.Graphics g,
                        int x,
                        int y,
                        int width,
                        int height)

Overrides:

paintBorder in class javax.swing.border.EmptyBorder

setFontHeight

void setFontHeight(int newH)