edu.mit.csail.sdg.alloy4
Class OurSyntaxWidget

java.lang.Object
  edu.mit.csail.sdg.alloy4.OurSyntaxWidget

public final class OurSyntaxWidget
extends java.lang.Object

Graphical syntax-highlighting editor.

Thread Safety: Can be called only by the AWT event thread

Field Summary

Listeners	listeners The current list of listeners; possible events are { STATUS_CHANGE, FOCUSED, CTRL_PAGE_UP, CTRL_PAGE_DOWN, CARET_MOVED }.
javax.swing.JComponent	obj1 This is an optional JComponent annotation.
javax.swing.JComponent	obj2 This is an optional JComponent annotation.

Constructor Summary

OurSyntaxWidget()
Constructs a syntax-highlighting widget.

OurSyntaxWidget(boolean enableSyntax, java.lang.String text, java.lang.String fontName, int fontSize, int tabSize, javax.swing.JComponent obj1, javax.swing.JComponent obj2)
Constructs a syntax-highlighting widget.

Method Summary

void	addTo(javax.swing.JComponent newParent, java.lang.Object constraint) Add this object into the given container.
boolean	canRedo() Returns true if we can perform redo right now.
boolean	canUndo() Returns true if we can perform undo right now.
void	clearUndo() Clear the undo history.
void	copy() Copy the current selection into the clipboard.
void	cut() Cut the current selection into the clipboard.
int	getCaret() Return the caret position.
java.lang.String	getFilename() Returns the filename.
int	getLineCount() Return the number of lines represented by the current text (where partial line counts as a line).
int	getLineOfOffset(int offset) Return the line number that the offset is in (If "offset" argument is too large, it will just return do_getLineCount()-1).
int	getLineStartOffset(int line) Return the starting offset of the given line (If "line" argument is too large, it will return the last line's starting offset)
java.lang.String	getText() Return the entire text.
boolean	isFile() Returns whether this textarea is based on an actual disk file.
boolean	modified() Returns the modified-or-not flag.
void	moveCaret(int a, int b) Select the content between offset a and offset b, and move the caret to offset b.
void	paste() Paste the current clipboard content.
void	redo() Perform redo if possible.
void	requestFocusInWindow() Transfer focus to this component.
void	setText(java.lang.String text) Change the entire text to the given text (and sets the modified flag)
void	undo() Perform undo if possible.

Methods inherited from class java.lang.Object

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

Field Detail

listeners

public final Listeners listeners

The current list of listeners; possible events are { STATUS_CHANGE, FOCUSED, CTRL_PAGE_UP, CTRL_PAGE_DOWN, CARET_MOVED }.

obj1

public final javax.swing.JComponent obj1

This is an optional JComponent annotation.

obj2

public final javax.swing.JComponent obj2

This is an optional JComponent annotation.

Constructor Detail

OurSyntaxWidget

public OurSyntaxWidget()

Constructs a syntax-highlighting widget.

OurSyntaxWidget

public OurSyntaxWidget(boolean enableSyntax,
                       java.lang.String text,
                       java.lang.String fontName,
                       int fontSize,
                       int tabSize,
                       javax.swing.JComponent obj1,
                       javax.swing.JComponent obj2)

Constructs a syntax-highlighting widget.

Method Detail

addTo

public void addTo(javax.swing.JComponent newParent,
                  java.lang.Object constraint)

Add this object into the given container.

getFilename

public java.lang.String getFilename()

Returns the filename.

modified

public boolean modified()

Returns the modified-or-not flag.

isFile

public boolean isFile()

Returns whether this textarea is based on an actual disk file.

getLineCount

public int getLineCount()

Return the number of lines represented by the current text (where partial line counts as a line).

For example: count("")==1, count("x")==1, count("x\n")==2, and count("x\ny")==2

getLineStartOffset

public int getLineStartOffset(int line)

Return the starting offset of the given line (If "line" argument is too large, it will return the last line's starting offset)

For example: given "ab\ncd\n", start(0)==0, start(1)==3, start(2...)==6. Same thing when given "ab\ncd\ne".

getLineOfOffset

public int getLineOfOffset(int offset)

Return the line number that the offset is in (If "offset" argument is too large, it will just return do_getLineCount()-1).

For example: given "ab\ncd\n", offset(0..2)==0, offset(3..5)==1, offset(6..)==2. Same thing when given "ab\ncd\ne".

canUndo

public boolean canUndo()

Returns true if we can perform undo right now.

canRedo

public boolean canRedo()

Returns true if we can perform redo right now.

undo

public void undo()

Perform undo if possible.

redo

public void redo()

Perform redo if possible.

clearUndo

public void clearUndo()

Clear the undo history.

getCaret

public int getCaret()

Return the caret position.

moveCaret

public void moveCaret(int a,
                      int b)

Select the content between offset a and offset b, and move the caret to offset b.

getText

public java.lang.String getText()

Return the entire text.

setText

public void setText(java.lang.String text)

Change the entire text to the given text (and sets the modified flag)

copy

public void copy()

Copy the current selection into the clipboard.

cut

public void cut()

Cut the current selection into the clipboard.

paste

public void paste()

Paste the current clipboard content.

requestFocusInWindow

public void requestFocusInWindow()

Transfer focus to this component.