package edu.princeton.swing.text;
import java.awt.*;
import java.awt.event.*;
import javax.swing.event.*;
import java.util.HashSet;
import java.util.Vector;
import java.util.Iterator;
import edu.princeton.toy.*;
import edu.princeton.toy.lang.*;
/**
* HighlightedDocument is an abstract representation of a document which supports syntax
* highlighting. This document can then be displayed with a THighlightedTextArea.
*
* @author Brian Tsang
* @version 7.1
*/
public abstract class HighlightedDocument
{
/**
* The allowed character with the greatest integer encoding.
*/
public static final char MAX_ALLOWED_CHARACTER = (char)126;
/**
* An array of all characters allowed in a HighlightedDocument.
*/
public static final boolean CHARACTER_ALLOWED[] = new boolean[MAX_ALLOWED_CHARACTER + 1];
private HashSet positions;
private Vector textListeners;
private Vector undoableEditListeners;
protected char chars[];
protected byte charStyles[];
protected int charCount;
protected int lineOffsets[];
protected int lineCount;
protected int maxLineLength;
private Thread writer;
private int readerCount;
private int positionCtr;
private UndoableEdit undoableEdit;
/**
* Initialize the ALLOWED_CHARACTERS array.
*/
static
{
CHARACTER_ALLOWED['\n'] = true;
for (int ctr = 32; ctr <= 126; ctr++)
CHARACTER_ALLOWED[ctr] = true;
}
/**
* Constructs a HighlightedDocument.
*/
public HighlightedDocument()
{
positions = new HashSet();
textListeners = new Vector();
undoableEditListeners = new Vector();
chars = new char[100000];
charStyles = new byte[100000];
charCount = 0;
lineOffsets = new int[10000];
lineCount = 0;
maxLineLength = 0;
writer = null;
readerCount = 0;
positionCtr = 0;
}
/**
* Returns the number of distinct styles used by this type of document. This must always
* return the same number.
*
* @return The number of distinct styles used by this type of document.
*/
public abstract int getStyleCount();
/**
* Returns the number of spaces to replace all tabs with.
*
* @return The number of spaces to replace all tabs with.
*/
public abstract int getTabSize();
/**
* Adds a listener to monitor changes in the text of the document.
*
* @param listener The listener to add to this document. A null value will cause a
* NullPointerException.
*/
public void addTextListener(TextListener listener)
{
if (listener == null)
throw new NullPointerException();
try
{
writeLock();
textListeners.add(listener);
}
finally
{
writeUnlock();
}
}
/**
* Removes a listener from this document. Nothing will happen if no match was found.
*
* @param listener The listener to remove from this document. A null value will cause a
* NullPointerException.
*/
public void removeTextListener(TextListener listener)
{
if (listener == null)
throw new NullPointerException();
try
{
writeLock();
textListeners.remove(listener);
}
finally
{
writeUnlock();
}
}
/**
* Adds a listener to monitor undoable changes in the document. Duplicates will be ignored.
*
* @param listener The listener to add to this document. A null value will cause a
* NullPointerException.
*/
public void addUndoableEditListener(UndoableEditListener listener)
{
if (listener == null)
throw new NullPointerException();
try
{
writeLock();
undoableEditListeners.add(listener);
}
finally
{
writeUnlock();
}
}
/**
* Removes a listener from this document. Nothing will happen if no match was found.
*
* @param listener The listener to remove from this document. A null value will cause a
* NullPointerException.
*/
public void removeUndoableEditListener(UndoableEditListener listener)
{
if (listener == null)
throw new NullPointerException();
try
{
writeLock();
undoableEditListeners.remove(listener);
}
finally
{
writeUnlock();
}
}
/**
* Creates a position at a given offset which will move with the text.
*
* @param offset The offset at which the position will start.
* @return The position object which will move with the text.
*/
public Position createPosition(int offset)
{
Position answer = null;
if (offset < 0)
throw new IllegalArgumentException();
try
{
writeLock();
if (offset > charCount)
offset = charCount;
answer = new Position(positionCtr, offset);
positions.add(answer);
positionCtr++;
}
finally
{
writeUnlock();
}
return answer;
}
/**
* Frees a position from future updates.
*
* @param position The position object to be detached.
*/
public void freePosition(Position position)
{
if (position == null)
throw new NullPointerException();
try
{
writeLock();
positions.remove(position);
}
finally
{
writeUnlock();
}
}
/**
* Creates a position triplet.
*
* @return The position triplet.
*/
public PositionTriplet createPositionTriplet()
{
PositionTriplet answer = null;
try
{
writeLock();
answer = new PositionTriplet(
new Position(positionCtr , 0),
new Position(positionCtr + 1, 0),
new Position(positionCtr + 2, 0)
);
positions.add(answer.selectionDot);
positions.add(answer.selectionMark);
positions.add(answer.caretPosition);
positionCtr += 3;
}
finally
{
writeUnlock();
}
return answer;
}
/**
* Frees a position triplet from future updates.
*
* @param positionTriplet The positionTriplet object to be detached.
*/
public void freePositionTriplet(PositionTriplet positionTriplet)
{
if (positionTriplet == null)
throw new NullPointerException();
try
{
writeLock();
positions.remove(positionTriplet.selectionDot);
positions.remove(positionTriplet.selectionMark);
positions.remove(positionTriplet.caretPosition);
}
finally
{
writeUnlock();
}
}
/**
* Returns an integer array containing a backup image of the position HashSet.
*/
protected int[] getPositionOffsets()
{
try
{
readLock();
Iterator iterator = positions.iterator();
int positionOffsets[] = new int[positionCtr];
while (iterator.hasNext())
{
Position position = (Position)iterator.next();
positionOffsets[position.id] = position.offset;
}
return positionOffsets;
}
finally
{
readUnlock();
}
}
/**
* Removes a segment of text specified by its offset and length. A TextEvent will be dispatched
* to the listeners.
*
* @param offset The index of the start of the segment to remove.
* @param length The length of the segment to remove.
* @param mergable Wheter or not the UndoableEdit generated can be merged with appropriately
* similar mergable UndoableEdits.
*/
public void remove(int offset, int length, boolean mergable)
{
replace(offset, length, "", mergable, true, null, false);
}
/**
* Inserts a string at the specified index. A TextEvent and an UndoableEditEvent will be
* dispatched to the listeners.
*
* @param offset The index at which to insert the string.
* @param string The string to insert.
* @param mergable Wheter or not the UndoableEdit generated can be merged with appropriately
* similar mergable UndoableEdits.
*/
public void insertString(int offset, String string, boolean mergable)
{
replace(offset, 0, string, mergable, true, null, false);
}
/**
* Replaces the text in a given range with the specified string. A TextEvent and an
* UndoableEditEvent will be dispatched to the listeners.
*
* @param offset The offset of the range about to be replaced.
* @param length The length of the range about to be replaced.
* @param string The string with which to replace the range.
* @param mergable Wheter or not the UndoableEdit generated can be merged with appropriately
* similar mergable UndoableEdits.
*/
public void replace(int offset, int length, String string, boolean mergable)
{
replace(offset, length, string, mergable, true, null, false);
}
/**
* Sets the text to the given string. A TextEvent will be dispatched to the listeners.
*
* @param string The string replace the old text with.
*/
public void setText(String string)
{
replace(0, Integer.MAX_VALUE, string, false, true, new int[0], true);
}
protected void utilReplace(int offset, int length, StringBuffer buffer,
int newLength, int positionOffsets[],
boolean disablePositionUpdate) {
// Replace the characters
char oldChars[] = chars;
int difference = newLength - length;
// Expand the array if necessary
if (charCount + difference > chars.length)
{
chars = new char[2 * (charCount + difference)];
charStyles = new byte[2 * (charCount + difference)];
for (int ctr = 0; ctr < offset; ctr++)
chars[ctr] = oldChars[ctr];
}
// Shift the characters after the replace range, if necessary
if (difference != 0 || chars != oldChars)
{
if (difference > 0)
{
int stopIndex = offset + length;
for (int ctr = charCount - 1; ctr >= stopIndex; ctr--)
chars[ctr + difference] = oldChars[ctr];
}
else {
for (int ctr = offset + length; ctr < charCount; ctr++)
chars[ctr + difference] = oldChars[ctr];
}
}
// Copy the new characters from the buffer onto the character array
buffer.getChars(0, newLength, chars, offset);
charCount += difference;
// Update the line structure
lineOffsets[0] = (int)0;
lineCount = 1;
for (int ctr = 0; ctr < charCount; ctr++)
{
if (chars[ctr] == '\n')
{
if (lineCount == lineOffsets.length)
{
int oldLineOffsets[] = lineOffsets;
lineOffsets = new int[lineCount * 2];
for (int ctr2 = 0; ctr2 < lineCount; ctr2++)
lineOffsets[ctr2] = oldLineOffsets[ctr2];
}
lineOffsets[lineCount] = (int)(ctr + 1);
lineCount++;
}
}
maxLineLength = charCount - lineOffsets[lineCount - 1];
for (int ctr = 0; ctr < lineCount - 1; ctr++)
{
int lineLength = lineOffsets[ctr + 1] - lineOffsets[ctr] - 1;
if (lineLength > maxLineLength)
maxLineLength = lineLength;
}
// Update the styles
assignStyles();
if (!positions.isEmpty())
{
// Restore the positions if necessary
if (positionOffsets != null)
{
Iterator iterator = positions.iterator();
while (iterator.hasNext())
{
Position position = (Position)iterator.next();
if (position.id < positionOffsets.length)
{
// If the offset is known, restore it
position.offset = positionOffsets[position.id];
}
else {
// Otherwise, set it to 0
position.offset = 0;
}
}
}
// Update the positions
if (!disablePositionUpdate)
{
Iterator iterator = positions.iterator();
while (iterator.hasNext())
{
Position position = (Position)iterator.next();
int positionOffset = position.offset;
if (positionOffset >= offset + length)
{
// The position was to the right of the range, shift it by the
// difference
position.offset = positionOffset + difference;
}
else if (positionOffset >= offset)
{
// The position was in the range, move it to the end of the replacement
// text
position.offset = offset + newLength;
}
else {
// Do nothing
}
}
}
// Restoring position offsets and disabling the position update are dangerous
// actions. We simply have to double check the work.
if (positionOffsets != null || disablePositionUpdate)
{
Iterator iterator = positions.iterator();
while (iterator.hasNext())
{
Position position = (Position)iterator.next();
int positionOffset = position.offset;
if (positionOffset >= charCount)
{
// The position was too large
position.offset = charCount;
}
else if (positionOffset < 0)
{
// The position was too small
position.offset = 0;
}
else {
// Do nothing
}
}
}
}
}
private String replaceString(String oldStr, String newStr, int index, int count) {
StringBuilder sb = new StringBuilder();
char[] charArray = oldStr.toCharArray();
sb.append(charArray , 0, index).append(newStr);
sb.append(charArray, index + count, charArray.length - (index + count));
return sb.toString();
}
/**
* Replaces the text in a given range with the specified string. And moves the positions around
* (if a positions array is specified). A TextEvent and an UndoableEditEvent will be
* dispatched to the listeners.
*
* @param offset The offset of the range about to be replaced.
* @param length The length of the range about to be replaced.
* @param string The string with which to replace the range.
* @param mergable Wheter or not the UndoableEdit generated can be merged with appropriately
* similar mergable UndoableEdits.
* @param positionOffsets An id-indexed array of position offsets to restore (this will be done
* before the position adjustment step). Leave as null if positions should be moved around
* normally.
* @param disablePositionUpdate Wheter or not to disable position update.
*/
protected void replace(int offset, int length, String string, boolean mergable,
boolean generateUndoEvent, int positionOffsets[],
boolean disablePositionUpdate)
{
if (offset < 0 || length < 0)
throw new IllegalArgumentException();
if (string == null)
throw new NullPointerException();
// remove non-standard characters
StringBuffer buffer = filterString(string);
int newLength = buffer.length();
if (length == 0 && newLength == 0 && positions == null)
return;
try
{
writeLock();
// if insertion offset is after last character in the document
if (offset > charCount)
offset = charCount;
// if the replacement range exceeds the document end
if (offset + length > charCount)
length = charCount - offset;
if (length == 0 && newLength == 0 && positions == null)
return;
//~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
// (1) take a snapshot for the Undo
String charsStr = new String(chars, 0, charCount);
StringBuffer textBefore = new StringBuffer(charsStr);
// (2) Insert the string without intervention
utilReplace(offset, length, buffer, newLength, positionOffsets, disablePositionUpdate);
// (3) Important computations
int lineStart = offset - offsetToCoordinate(offset).x;;
int lineEnd = coordinateToOffset(Integer.MAX_VALUE, offsetToCoordinate(offset + string.length()).y);
String newLines = getText(lineStart, lineEnd);
// (4) Parse every line in the new lines and insert pseudocode where needed
String oldLines = new String(newLines);
int index = 0;
int oldIndex = 0;
boolean changed = false;
while (index < newLines.length()) {
// read a line
StringBuilder line = new StringBuilder();
while (index < newLines.length() && newLines.charAt(index) != '\n') {
line.append(newLines.charAt(index));
index++;
}
// Check if this line needs pseudocode
int lineLength = line.length();
TWord command;
String pseudoCodeString = "";
boolean needsPseudo = true;
if (lineLength < 8) {
// line too short to have an instruction
needsPseudo = false;
}
else if (!isCommand(line.substring(0, 8))) {
// no instruction
needsPseudo = false;
}
// Update the line only if it needs a pseudocode
if (needsPseudo) {
String commentedLine = TWord.commentLine(line.toString());
if (!commentedLine.equals(line.toString())) {
index += commentedLine.length() - line.length();
newLines = replaceString(newLines, commentedLine, oldIndex, line.length());
changed = true;
}
}
// bypass the \n
index++;
oldIndex = index;
}
if (changed) {
StringBuffer bf = new StringBuffer(newLines);
utilReplace(lineStart, oldLines.length(), bf, bf.length(), positionOffsets, disablePositionUpdate);
}
// Dispatch the events
if (!textListeners.isEmpty())
{
TextEvent e = new TextEvent(this, TextEvent.TEXT_VALUE_CHANGED);
Object array[] = textListeners.toArray();
for (int ctr = 0; ctr < array.length; ctr++)
((TextListener)array[ctr]).textValueChanged(e);
}
if (generateUndoEvent && !undoableEditListeners.isEmpty())
{
// take a snapshot of the current text document
charsStr = new String(chars, 0, charCount);
StringBuffer textAfter = new StringBuffer(charsStr);
// create an undo command
javax.swing.undo.UndoableEdit undoableEdit = null;
undoableEdit = new UndoableEdit(0, textBefore, textAfter, mergable);
UndoableEditEvent e = new UndoableEditEvent(this, undoableEdit);
Object array[] = undoableEditListeners.toArray();
for (int ctr = 0; ctr < array.length; ctr++)
((UndoableEditListener)array[ctr]).undoableEditHappened(e);
}
}
finally
{
writeUnlock();
}
}
/**
* check if the given string is a TOY instruction
*/
private boolean isCommand(String str) {
if (str.length() > 8)
return false;
for (int i = 0; i < str.length(); i++) {
if ((i < 2 || i > 3) &&
(!TWord.isHexDigit(str.charAt(i))))
return false;
else if (i == 2 && str.charAt(i) != ':')
return false;
else if (i == 3 && str.charAt(i) != ' ')
return false;
}
return true;
}
/**
* Updates the charStyles array based on chars, charCount, lineOffsets, and lineCount. The
* implementation should assume that a write lock will have been obtained by the caller of this
* function.
*/
protected abstract void assignStyles();
/**
* Filters out all "non-standard" ASCII characters from the string.
*
* @param string The string to be filtered. A null value will result in a NullPointerException.
* @return A StringBuffer containing the original string, without any "non-standard" ASCII
* characters.
*/
public StringBuffer filterString(String string)
{
int length = string.length();
StringBuffer buffer = new StringBuffer(2 * length);
// Traslate mac/windows newline styles and extended ASCII characters
for (int ctr = 0; ctr < length; ctr++)
{
char character = string.charAt(ctr);
switch (character)
{
// Translate Mac extended characters
case (char)212: // standard '
case (char)213: // backward '
buffer.append('\'');
break;
case (char)210: // opening "
case (char)211: // closing "
buffer.append('\"');
break;
// Translate Windows extended characters
case (char)8216: // standard '
case (char)8217: // backward '
buffer.append('\'');
break;
case (char)8220: // opening "
case (char)8221: // closing "
buffer.append('\"');
break;
// Convert carriage-returns to UNIX-style newlines
case '\r':
if (ctr + 1 < length && string.charAt(ctr + 1) == '\n')
{
// Windows uses "\r\n"
buffer.append('\n');
ctr++;
}
else {
// Mac uses "\r"
buffer.append('\n');
}
break;
// Convert tabs into getTabSize() spaces
case '\t':
{
int tabSize = getTabSize();
for (int ctr2 = 0; ctr2 < tabSize; ctr2++)
buffer.append(' ');
}
break;
// Only allow the printable ASCII characters as well as the space and newline
default:
// Only accept newlines, or printable ASCII
if (character <= MAX_ALLOWED_CHARACTER && CHARACTER_ALLOWED[character])
{
buffer.append(character);
}
}
}
return buffer;
}
/**
* Returns the text of the document.
*
* @return The text of the document.
*/
public String getText()
{
return getText(0, Integer.MAX_VALUE);
}
/**
* Returns part of the text of the document.
*
* @param start The offset at which to begin.
* @param end The offset at which to end.
* @return The text of the document.
*/
public String getText(int start, int end)
{
String answer;
if (start < 0 || start > end)
throw new IllegalArgumentException();
if (start == end)
return "";
try
{
readLock();
if (start > charCount)
start = charCount;
if (end > charCount)
end = charCount;
answer = new String(chars, start, end - start);
}
finally
{
readUnlock();
}
return answer;
}
/**
* Returns the number of characters in the document.
*
* @return The number of characters in the document.
*/
public int getLength()
{
int answer;
try
{
readLock();
answer = charCount;
}
finally
{
readUnlock();
}
return answer;
}
/**
* Returns the number of lines in the document.
*
* @return The number of lines in the document.
*/
public int getLineCount()
{
int answer;
try
{
readLock();
answer = lineCount;
}
finally
{
readUnlock();
}
return answer;
}
/**
* Returns the length of the longest line.
*
* @return The length of the longest line.
*/
public int getMaxLineLength()
{
int answer;
try
{
readLock();
answer = maxLineLength;
}
finally
{
readUnlock();
}
return answer;
}
/**
* Returns the bounds of the word containing the character at the given offset. The following
* are the rules used to get the word bounds:
* - If that character is a newline, the bounds will enclose that one newline.
*
- If that character is a space, the bounds will enclose all spaces adjacent to that space.
*
- If that character is an identifier character (letter, digit, or underscore), then the
* bounds will enclose all identifier characters adjacent to that character.
*
- If that charater is something else, the bounds will just enclose all identical
* characters adjacent to that character.
*
*
* @param offset The offset of one of the characters in the desired word.
* @return The bounds (a integer array of size 2) of the word. The word will span the
* half-open interval [retVal[0], retVal[1]).
*/
public int[] getWordBounds(int offset)
{
int answer[] = new int[2];
if (offset < 0)
throw new IllegalArgumentException();
try
{
readLock();
if (offset >= charCount)
{
answer[0] = charCount;
answer[1] = charCount;
}
else {
char ch = chars[offset];
if (ch == '\n')
{
answer[0] = offset;
answer[1] = offset + 1;
}
else if (ch == ' ')
{
int start = offset;
int end = offset + 1;
while (start > 0 && chars[start - 1] == ' ')
start--;
while (end < charCount && chars[end] == ' ')
end++;
answer[0] = start;
answer[1] = end;
}
else if (Character.isLetterOrDigit(ch) || ch == '_')
{
int start = offset;
int end = offset + 1;
while (start > 0 &&
(Character.isLetterOrDigit(chars[start - 1]) || chars[start - 1] == '_'))
start--;
while (end < charCount &&
(Character.isLetterOrDigit(chars[end]) || chars[end] == '_'))
end++;
answer[0] = start;
answer[1] = end;
}
else {
int start = offset;
int end = offset + 1;
while (start > 0 && chars[start - 1] == ch)
start--;
while (end < charCount && chars[end] == ch)
end++;
answer[0] = start;
answer[1] = end;
}
}
}
finally
{
readUnlock();
}
return answer;
}
/**
* Obtains a read lock and passes the protected data to an implementation of
* HighlightedDocumentRenderer. The implementation of HighlightedDocumentRenderer should not
* modify the data or presume that it will be valid after the method returns.
*
* @param renderer The renderer that will recieve access to the protected data.
* @param extraInfo An object to hold additional parameters from the caller of allowRender.
* @see HighlightedDocumentRenderer#doRender(char[], byte[], int, int[], int, Object)
*/
public void allowRender(HighlightedDocumentRenderer renderer, Object extraInfo)
{
if (renderer == null)
throw new NullPointerException();
try
{
readLock();
renderer.doRender(chars, charStyles, charCount, lineOffsets, lineCount, extraInfo);
}
finally
{
readUnlock();
}
}
/**
* Takes a (column, line) pair and returns the nearest valid offset.
*
* @param p The point (where x is the column, and y is the line) to convert to an offset.
* @return The nearest valid offset for the coordinate.
*/
public int coordinateToOffset(Point p)
{
return coordinateToOffset(p.x, p.y);
}
/**
* Takes a (column, line) pair and returns the nearest valid offset.
*
* @param column The column of the coordinate to convert to an offset.
* @param line The line of the coordinate to convert to an offset.
* @return The nearest valid offset for the coordinate.
*/
public int coordinateToOffset(int column, int line)
{
int answer = 0;
try
{
readLock();
if (line < 0)
line = 0;
if (line >= lineCount)
line = lineCount - 1;
int lineLength;
if (line == lineCount - 1)
lineLength = charCount - lineOffsets[line];
else
lineLength = lineOffsets[line + 1] - lineOffsets[line] - 1;
if (column < 0)
column = 0;
if (column > lineLength)
column = lineLength;
answer = lineOffsets[line] + column;
}
finally
{
readUnlock();
}
return answer;
}
/**
* Takes an offset and returns the nearest valid (column, line) pair.
*
* @param offset The offset to convert to a coordinate.
* @return The nearest valid point (where x is the column, and y is the line) to corresponding
* to the given offset.
*/
public Point offsetToCoordinate(int offset)
{
Point answer = new Point();
try
{
readLock();
if (offset < 0)
offset = 0;
if (offset > charCount)
offset = charCount;
int line = 0;
while (line + 1 < lineCount && offset >= lineOffsets[line + 1])
line++;
answer.x = offset - lineOffsets[line];
answer.y = line;
}
finally
{
readUnlock();
}
return answer;
}
/**
* Obtains a write-lock for this HighlightedDocument. While this Thread has a write-lock, all
* Threads requesting either a read or write lock will be suspended. A call to this should be
* followed by a call to writeUnlock() in a finally block:
* try
* {
* writeLock();
*
* ...
* }
* finally
* {
* writeUnlock();
* }
*
* @see #writeUnlock()
* @see #readLock()
* @see #readUnlock()
*/
protected synchronized final void writeLock()
{
try
{
while (readerCount > 0 || writer != null)
{
if (Thread.currentThread() == writer)
throw new RuntimeException("DocumentListener attempted to mutate");
wait();
}
writer = Thread.currentThread();
}
catch (InterruptedException e)
{
throw new RuntimeException("Interrupted attempt to aquire write lock");
}
}
/**
* Releases the write-lock for this HighlightedDocument.
*
* @see #writeLock()
* @see #readLock()
* @see #readUnlock()
*/
protected synchronized final void writeUnlock()
{
writer = null;
notifyAll();
}
/**
* Obtains a read-lock for this HighlightedDocument. While this Thread has a read-lock, all
* Threads requesting a write lock will be suspended. A call to this should be followed by a
* call to readUnlock() in a finally block:
* try
* {
* readLock();
*
* ...
* }
* finally
* {
* readUnlock();
* }
*
* @see #writeLock()
* @see #writeUnlock()
* @see #readUnlock()
*/
protected synchronized final void readLock()
{
try
{
while (writer != null)
{
if (writer == Thread.currentThread())
return;
wait();
}
readerCount++;
}
catch (InterruptedException e)
{
throw new RuntimeException("Interrupted attempt to aquire read lock");
}
}
/**
* Releases the read-lock for this HighlightedDocument.
*
* @see #writeLock()
* @see #writeUnlock()
* @see #readLock()
*/
protected synchronized final void readUnlock()
{
if (writer == Thread.currentThread())
return;
int index = -1;
readerCount--;
if (readerCount < 0)
throw new RuntimeException("Bad reader count");
}
/**
* UndoableEdit is a simple implementation of javax.swing.undo.UndoableEdit.
*
* @author btsang
* @version 7.1
*/
public class UndoableEdit implements javax.swing.undo.UndoableEdit
{
private HighlightedDocument document;
private int offset;
private StringBuffer oldText;
private StringBuffer newText;
private int positionOffsets[];
private boolean mergable;
private boolean undoable;
protected UndoableEdit(int offset, StringBuffer oldText, StringBuffer newText, boolean mergable) {
if (newText == null)
throw new NullPointerException();
if (offset < 0)
throw new IllegalArgumentException();
this.document = HighlightedDocument.this;
this.newText = newText;
this.mergable = mergable;
this.oldText = oldText;
this.offset = offset;
}
/**
* Creates a new UndoableEdit. This should be called *before* the edit is actually
* performed.
*/
protected UndoableEdit(int offset, int length, StringBuffer newText, boolean mergable)
{
if (newText == null)
throw new NullPointerException();
if (length < 0 || offset < 0)
throw new IllegalArgumentException();
document = HighlightedDocument.this;
this.newText = newText;
this.mergable = mergable;
try
{
readLock();
if (offset > charCount)
offset = charCount;
this.offset = offset;
if (length + offset > charCount)
length = charCount - offset;
if (length == 0)
{
oldText = new StringBuffer();
}
else {
oldText = new StringBuffer(2 * length);
oldText.append(chars, offset, length);
}
positionOffsets = getPositionOffsets();
}
finally
{
readUnlock();
}
}
/**
* Attempts to merge another edit with the current edit.
*/
public boolean addEdit(javax.swing.undo.UndoableEdit edit)
{
if (document == null)
throw new IllegalStateException();
if (mergable && edit != null && edit instanceof UndoableEdit)
{
UndoableEdit undoableEdit = (UndoableEdit)edit;
if (undoableEdit.mergable && undoableEdit.document == document)
{
// Are they mergable insertions?
if (oldText.length() == 0 && undoableEdit.oldText.length() == 0)
{
int newTextLength = newText.length();
// Does this new text immediately follow our new text, and does this new
// text contain the same material (whitespace / non-whitespace) as ours?
if (undoableEdit.offset == offset + newTextLength &&
(newTextLength == 0 || undoableEdit.newText.length() == 0 ||
(Character.isWhitespace(newText.charAt(newTextLength - 1)) ==
Character.isWhitespace(undoableEdit.newText.charAt(0)))))
{
newText.append(undoableEdit.newText);
undoableEdit.die();
return true;
}
}
// Are they mergable removals?
if (newText.length() == 0 && undoableEdit.newText.length() == 0)
{
// Does this removal immediately follow our previous removal?
if (undoableEdit.offset == offset)
{
oldText.append(undoableEdit.oldText);
undoableEdit.die();
return true;
}
// Does this removal immediately precede our previous removal?
if (undoableEdit.offset + oldText.length() == offset)
{
oldText.insert(0, undoableEdit.oldText);
offset = undoableEdit.offset;
undoableEdit.die();
return true;
}
}
// Are they mergable replacements (from editing in non-insert mode)?
if (newText.length() == oldText.length() &&
undoableEdit.newText.length() == undoableEdit.oldText.length())
{
int newTextLength = newText.length();
// Does this new text immediately follow our new text, and does this new
// text contain the same material (whitespace / non-whitespace) as ours?
if (undoableEdit.offset == offset + newTextLength &&
(newTextLength == 0 || undoableEdit.newText.length() == 0 ||
(Character.isWhitespace(newText.charAt(newTextLength - 1)) ==
Character.isWhitespace(undoableEdit.newText.charAt(0)))))
{
newText.append(undoableEdit.newText);
oldText.append(undoableEdit.oldText);
undoableEdit.die();
return true;
}
}
}
}
return false;
}
/**
* Returns wheter or not this edit is alive.
*/
public boolean canRedo()
{
return (document != null);
}
/**
* Returns wheter or not this edit is alive.
*/
public boolean canUndo()
{
return (document != null);
}
/**
* Frees resources associated with an edit.
*/
public void die()
{
document = null;
oldText = null;
newText = null;
positionOffsets = null;
}
/**
* Returns a string describing the edit.
*/
public String getPresentationName()
{
return (mergable?"Mergeable ":"") + "UndoableEdit (" + offset + ", \"" + oldText +
"\", \"" + newText + "\")";
}
/**
* Returns a string describing the edit.
*/
public String getRedoPresentationName()
{
return getPresentationName();
}
/**
* Returns a string describing the edit.
*/
public String getUndoPresentationName()
{
return getPresentationName();
}
/**
* Returns a string describing the edit.
*/
public String toString()
{
return getPresentationName();
}
/**
* Returns true (this edit involved a document mutation).
*/
public boolean isSignificant()
{
return true;
}
/**
* Redoes an edit.
*/
public void redo()
{
if (document == null)
throw new IllegalStateException();
replace(
offset,
oldText.length(),
newText.toString(),
false,
false,
positionOffsets,
false
);
}
/**
* Returns false (this edit should never replace another).
*/
public boolean replaceEdit(javax.swing.undo.UndoableEdit anEdit)
{
return false;
}
/**
* Undoes this edit.
*/
public void undo()
{
if (document == null)
throw new IllegalStateException();
replace(
offset,
newText.length(),
oldText.toString(),
false,
false,
positionOffsets,
true
);
}
}
/**
* Position is a simple implementation of javax.swing.text.Position.
*/
public class Position implements javax.swing.text.Position
{
protected int id;
protected int offset;
/**
* Instantiates a new Position.
*/
protected Position(int id, int offset)
{
this.id = id;
this.offset = offset;
}
/**
* Sets the offset encapsulated by this Position. If the offset is out of bounds, the
* the offset will be silently corrected.
*
* @param offset The new offset this Position should return.
*/
public void setOffset(int offset)
{
if (this.offset == offset)
return;
try
{
readLock();
if (offset < 0)
{
this.offset = 0;
}
else if (offset > charCount)
{
this.offset = charCount;
}
else {
this.offset = offset;
}
}
finally
{
readUnlock();
}
}
/**
* Returns the offset encapsulated by this Position.
*
* @return The offset represented by this Position.
*/
public int getOffset()
{
return offset;
}
}
/**
* PositionTriplet maintains three positions which permits efficient synchronous changes.
*
* @author btsang
* @version 7.1
*/
public class PositionTriplet
{
/**
* The value to pass to set so that the specified position's offset will not change.
*/
public static final int NO_CHANGE = Integer.MIN_VALUE;
protected Position selectionDot, selectionMark, caretPosition;
/**
* Creates a new PositionTriplet.
*/
protected PositionTriplet(Position selectionDot, Position selectionMark,
Position caretPosition)
{
if (selectionDot == null || selectionMark == null || caretPosition == null)
throw new NullPointerException();
this.selectionDot = selectionDot;
this.selectionMark = selectionMark;
this.caretPosition = caretPosition;
}
/**
* Moves the offsets of the triplets to the valid position nearest to the specified offset.
* Pass the NO_CHANGE value to leave an offset as it is.
*
* @param selectionDotOffset The new offset for the selectionDot.
* @param selectionMarkOffset The new offset for the selectionMark.
* @param caretPositionOffset The new offset for the caretPosition.
*/
public void set(int selectionDotOffset, int selectionMarkOffset, int caretPositionOffset)
{
try
{
readLock();
if (selectionDotOffset != NO_CHANGE)
{
if (selectionDotOffset < 0)
{
selectionDot.offset = 0;
}
else if (selectionDotOffset > charCount)
{
selectionDot.offset = charCount;
}
else {
selectionDot.offset = selectionDotOffset;
}
}
if (selectionMarkOffset != NO_CHANGE)
{
if (selectionMarkOffset < 0)
{
selectionMark.offset = 0;
}
else if (selectionMarkOffset > charCount)
{
selectionMark.offset = charCount;
}
else {
selectionMark.offset = selectionMarkOffset;
}
}
if (caretPositionOffset != NO_CHANGE)
{
if (caretPositionOffset < 0)
{
caretPosition.offset = 0;
}
else if (caretPositionOffset > charCount)
{
caretPosition.offset = charCount;
}
else {
caretPosition.offset = caretPositionOffset;
}
}
}
finally
{
readUnlock();
}
}
/**
* Returns the offset of the selectionDot.
*
* @return The offset of the selectionDot.
*/
public int getSelectionDotOffset()
{
return selectionDot.offset;
}
/**
* Returns the offset of the selectionMark.
*
* @return The offset of the selectionMark.
*/
public int getSelectionMarkOffset()
{
return selectionMark.offset;
}
/**
* Returns the offset of the caretPosition.
*
* @return The offset of the caretPosition.
*/
public int getCaretPositionOffset()
{
return caretPosition.offset;
}
/**
* Returns the lesser of the offsets of the selectionDot and selectionMark.
*
* @return The lesser of the offsets of the selectionDot and selectionMark.
*/
public int getSelectionStartOffset()
{
return Math.min(selectionDot.offset, selectionMark.offset);
}
/**
* Returns the greater of the offsets of the selectionDot and selectionMark.
*
* @return The greater of the offsets of the selectionDot and selectionMark.
*/
public int getSelectionEndOffset()
{
return Math.max(selectionDot.offset, selectionMark.offset);
}
}
}