/* EditorFilter.java
* This file is part of source files of MEPer.
* It defines the behaviors of the editor.
*
* @author Shengjun Pan
*/
import java.awt.*;
import java.awt.event.*;
import javax.swing.*;
import javax.swing.text.*;
import java.util.*;
import javax.swing.undo.*;
public class EditorFilter extends DocumentFilter {
String[] keywords ={"beginfig","endfig","for","draw","drawarrow","endfor",
"def", "vardef", "enddef","if", "fi", "withcolor","fill",
"shifted", "scaled", "rotated", "withpen"};
String[] datatypes = {"picture","numeric","path","pair","transform","color",
"string", "boolean", "pen"};
int fontSize = 14;
HashMap<String,SimpleAttributeSet> tokenToAset;
JTextPane editor;
JButton saveButton;
public EditorFilter(JTextPane ed, JButton sb) {
editor = ed;
saveButton = sb;
tokenToAset = new HashMap<String,SimpleAttributeSet>();
SimpleAttributeSet aset= new SimpleAttributeSet();
StyleConstants.setForeground(aset, Color.BLUE);
StyleConstants.setBold(aset, true);
StyleConstants.setFontSize(aset,fontSize);
tokenToAset.put("keyword", aset);
aset= new SimpleAttributeSet();
StyleConstants.setForeground(aset, Color.GREEN);
StyleConstants.setBold(aset, true);
StyleConstants.setFontSize(aset,fontSize);
tokenToAset.put("digits", aset);
aset= new SimpleAttributeSet();
StyleConstants.setForeground(aset, Color.BLACK);
StyleConstants.setBold(aset, false);
StyleConstants.setFontSize(aset,fontSize);
tokenToAset.put("normal", aset);
aset= new SimpleAttributeSet();
StyleConstants.setForeground(aset, Color.GREEN);
StyleConstants.setBold(aset, true);
StyleConstants.setFontSize(aset,fontSize);
tokenToAset.put("datatype", aset);
aset= new SimpleAttributeSet();
StyleConstants.setForeground(aset, Color.MAGENTA);
StyleConstants.setBold(aset, true);
StyleConstants.setFontSize(aset,fontSize);
tokenToAset.put("quoted", aset);
//editor.addKeyListener(this);
editor.setFont(new Font(Font.MONOSPACED,Font.PLAIN,fontSize));
// enable undo/redo
final UndoManager undoManager = new UndoManager();
editor.getDocument().addUndoableEditListener(undoManager);
editor.getInputMap().put(KeyStroke.getKeyStroke("ctrl Z"), "undo");
editor.getActionMap().put("undo", new AbstractAction() {
public void actionPerformed(ActionEvent evt) {
try { undoManager.undo();}
catch (Throwable t) {Toolkit.getDefaultToolkit().beep();}
}});
editor.getInputMap().put(KeyStroke.getKeyStroke("ctrl R"), "redo");
editor.getActionMap().put("redo", new AbstractAction() {
public void actionPerformed(ActionEvent evt) {
try { undoManager.redo();}
catch (Throwable t) {Toolkit.getDefaultToolkit().beep();}
}});
}
@Override
public void insertString(FilterBypass fb, int offs,
String str, AttributeSet a)
throws BadLocationException {
saveButton.setEnabled(true);
highlightAndInsert(fb, offs, str);
}
@Override
public void replace(DocumentFilter.FilterBypass fb, int offs, int len,
String str, AttributeSet a) throws BadLocationException {
saveButton.setEnabled(true);
super.remove(fb, offs, len);
highlightAndInsert(fb,offs,str);
}
@Override
public void remove(DocumentFilter.FilterBypass fb, int offs, int len)
throws BadLocationException {
saveButton.setEnabled(true);
boolean removingWhite = fb.getDocument().getText(offs, len).trim().isEmpty();
super.remove(fb, offs, len);
String indent = "";
String smallerIndent ="";
try {
indent = indent(offs,false);
smallerIndent = indent(offs,true);
int newLineOffs = offs - indent.length()-1;
String maybeNewline=newLineOffs<0?"":editor.getDocument().getText(newLineOffs, 1);
if(removingWhite && indent.length()>0 && (maybeNewline.isEmpty() || maybeNewline.equals("\n"))){
super.remove(fb,newLineOffs+1, indent.length());
super.insertString(fb,newLineOffs+1,smallerIndent, tokenToAset.get("normal"));
} else if(offs>0) { highlightAndInsert(fb,offs,"");}
} catch(Throwable t) {}
}
private void highlightAndInsert(FilterBypass fb, int offs, String str)
throws BadLocationException {
// invoke automatical indentation only if a single <ENTER> is received.
// In the case of pasting multiple lines, the original indentation
// should be reserved.
if(str.length()==1 && str.charAt(0)=='\n') {
String indent = "";
try {
indent = indent(offs,false);
super.insertString(fb,offs, "\n"+indent, tokenToAset.get("normal"));
} catch(Throwable t) {}
return;
}
//translate
String newstr="";
for(int i=0;i<str.length(); i++){
char c= str.charAt(i);
switch(c) {
case '\t':
{
newstr += " ";
break;
}
default:
newstr += c;
}
}
String prefix, suffix;
// search for partial word before
int from=offs;
if (newstr.isEmpty() || !Character.isWhitespace(newstr.charAt(0))){
from --;
while(from >=0 ) {
char c = fb.getDocument().getText(from, 1).charAt(0);
if(Character.isWhitespace(c)){ break;}
from--;
}
from ++;
}
prefix = fb.getDocument().getText(from, offs-from);
// search for partial word after
int to=offs;
if (newstr.isEmpty() || !Character.isWhitespace(newstr.charAt(newstr.length()-1))){
int wholeLen = fb.getDocument().getLength();
while(to < wholeLen) {
char c = fb.getDocument().getText(to,1).charAt(0);
if(Character.isWhitespace(c)){break;}
to++;
}
}
suffix = fb.getDocument().getText(offs,to-offs);
// removing the partial words
offs -= prefix.length();
super.remove(fb, offs, prefix.length()+suffix.length());
String[] words = newstr.split(" ",-1);
words[0] = prefix + words[0];
words[words.length-1] += suffix;
newstr = prefix + newstr + suffix;
String state="normal";
if(offs>0){
Color fgcolor=StyleConstants.getForeground(editor.getStyledDocument().getCharacterElement(offs-1).getAttributes());
if (fgcolor.equals(StyleConstants.getForeground(tokenToAset.get("quoted"))))
state = "quoted";
}
String token="";
char c;
newstr += '\0';
for(int i=0;i< newstr.length();i++){
c = newstr.charAt(i);
String newstate="normal";
if(c=='\0') newstate = "done";
else if(state.equals("quoted")|| state.equals("lquote")) newstate= (c=='\"')? "rquote":"quoted";
else if(Character.isDigit(c)) newstate = "digits";
else if(Character.isLetter(c)) newstate = "word";
else if(c=='\"') newstate= "lquote";
if (!state.equals(newstate)) {
String key="normal";
if(state.equals("digits")) key="digits";
else if(state.equals("word") && isKeyword(token)) key="keyword";
else if(state.equals("word") && isDatatype(token)) key="datatype";
else if(state.equals("quoted")) key="quoted";
super.insertString(fb, offs, token, tokenToAset.get(key));
offs += token.length();
state = newstate;
token = "";
}
token +=c;
}
editor.setCaretPosition(offs-suffix.length());
}
// return the indent (as string of whitespaces) of the current line
// or closest shorter indent of previous lines if 'wantShorter' is true.
private String indent(int offs, boolean wantShorter) throws BadLocationException {
int pos=offs-1;
int pos_firstNonWhite = offs;
int firstIndentSize=-1;
while(pos>=0){
char ch= editor.getText(pos, 1).charAt(0);
if(ch=='\n') {
int previousIndentSize = pos_firstNonWhite-pos-1;
if(!wantShorter || previousIndentSize < firstIndentSize) break;
if(firstIndentSize<0) firstIndentSize = previousIndentSize;
pos_firstNonWhite = pos;
}
if(!Character.isWhitespace(ch)) {
pos_firstNonWhite = pos;
}
pos --;
}
return editor.getText(pos+1, pos_firstNonWhite-pos-1);
}
private boolean isKeyword(String word) {
for(int i=0;i<keywords.length;i++)
if(keywords[i].equals(word))
return true;
return false;
}
private boolean isDatatype(String word) {
for(int i=0;i<datatypes.length;i++)
if(datatypes[i].equals(word))
return true;
return false;
}
}