Skip to content
Permalink
master
Go to file
 
 
Cannot retrieve contributors at this time
455 lines (374 sloc) 10 KB
//==============================================================================
//
// Copyright (c) 2002-
// Authors:
// * Andrew Hinton <ug60axh@cs.bham.ac.uk> (University of Birmingham)
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
//
//------------------------------------------------------------------------------
//
// This file is part of PRISM.
//
// PRISM is free software; you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
//
// PRISM is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with PRISM; if not, write to the Free Software Foundation,
// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
//
//==============================================================================
package userinterface.model.pepaModel;
import javax.swing.*;
import javax.swing.text.*;
import javax.swing.undo.CannotRedoException;
import javax.swing.undo.CannotUndoException;
import javax.swing.undo.UndoManager;
import java.util.regex.*;
import java.awt.*;
import javax.swing.event.*;
import java.io.*;
import userinterface.model.*;
public class GUIPepaModelEditor extends GUIModelEditor implements DocumentListener
{
private JEditorPane editor;
private UndoManager undoManager;
private PlainDocument d;
private GUIMultiModelHandler handler;
/** Creates a new instance of GUIPepaModelEditor */
public GUIPepaModelEditor(GUIMultiModelHandler handler)
{
editor = new JEditorPane();
PepaEditorKit kit = new PepaEditorKit();
editor.setEditorKitForContentType("text/pepa", kit);
editor.setContentType("text/pepa");
undoManager = new UndoManager();
undoManager.setLimit(200);
//editor.setForeground(FOREGROUND_COLOR);
this.handler = handler;
d = (PlainDocument)editor.getDocument();
editor.getDocument().addDocumentListener(this);
initComponents();
}
private void initComponents()
{
JScrollPane scroller = new JScrollPane();
{
scroller.setViewportView(editor);
}
setLayout(new BorderLayout());
add(scroller, BorderLayout.CENTER);
}
public void changedUpdate(DocumentEvent e)
{
}
public void insertUpdate(DocumentEvent e)
{
if (handler != null)handler.hasModified(true);
}
public void removeUpdate(DocumentEvent e)
{
if (handler != null)handler.hasModified(true);
}
public String getParseText()
{
return editor.getText();
}
public void newModel()
{
editor.setText("");
}
public void read(Reader s, Object obj) throws IOException
{
editor.read(s, obj);
d = (PlainDocument)editor.getDocument();
d.addDocumentListener(this);
// System.out.println("here");
}
public void write(Writer s) throws IOException
{
editor.write(s);
}
/** Performs an undo operation on the text in the model editor.
*/
public void undo() {
try {
undoManager.undo();
} catch (CannotUndoException ex) {
//GUIPrism.getGUI().getMultiLogger().logMessage(PrismLogLevel.PRISM_ERROR, ex.getMessage());
}
}
/** Performs a redo operation on the text in the model editor.
*/
public void redo() {
try {
undoManager.redo();
} catch (CannotRedoException ex) {
//GUIPrism.getGUI().getMultiLogger().logMessage(PrismLogLevel.PRISM_ERROR, ex.getMessage());
}
}
public void copy()
{
editor.copy();
}
public void cut()
{
editor.cut();
}
public void paste()
{
editor.paste();
}
public void delete()
{
}
public void selectAll()
{
editor.selectAll();
}
public boolean isEditable()
{
return editor.isEditable();
}
public void setEditorFont(Font f)
{
editor.setFont(f);
}
public void setEditorBackground(Color c)
{
editor.setBackground(c);
}
class PepaEditorKit extends DefaultEditorKit
{
private PepaContext preferences;
/** Creates a new instance of PrismEditorKit */
public PepaEditorKit()
{
super();
}
public PepaContext getStylePreferences()
{
if (preferences == null)
{
preferences = new PepaContext();
}
return preferences;
}
public void setStylePreferences(PepaContext prefs)
{
preferences = prefs;
}
public String getContentType()
{
return "text/pepa";
}
public Document createDefaultDocument()
{
return new PlainDocument();
}
public final ViewFactory getViewFactory()
{
return getStylePreferences();
}
}
class PepaContext extends StyleContext implements ViewFactory
{
public static final String COMMENT_D = "Single Line Comment";
/** Creates a new instance of PrismContext */
public PepaContext()
{
super();
}
public View create(Element elem)
{
return new PepaView(elem);
}
}
static final userinterface.model.Style PLAIN_S = new userinterface.model.Style(Color.black, Font.PLAIN);
class PepaView extends PlainView
{
private Matcher match;
private Pattern pattern;
public PepaView(Element elem)
{
super(elem);
pattern = Pattern.compile("%.*");
}
public void paint(Graphics g, Shape a)
{
super.paint(g, a);
}
protected int drawUnselectedText(Graphics g, int x, int y,int p0, int p1) throws BadLocationException
{
int stLine = findStartOfLine(p0, getDocument());
int enLine = findEndOfLine(p1, getDocument());
if (g instanceof Graphics2D) {
Graphics2D g2d = (Graphics2D)g;
g2d.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING, RenderingHints.VALUE_TEXT_ANTIALIAS_ON);
}
try
{
g.setColor(Color.green);
Document doc = getDocument();
Segment segment = getLineBuffer();
//String s = doc.getText(p0, p1-p0);
String s = doc.getText(stLine, enLine-stLine);
userinterface.model.Style[] styles = highlight(s, (p0-stLine), (p1-p0));
int currStart = 0;
int currEnd = 0;
Color last = null;
String fname = handler.getPepaEditorFontFast().getName();
int fsize = handler.getPepaEditorFontFast().getSize();
for(int curr = 0; curr < styles.length; curr++)
{
userinterface.model.Style c = styles[curr];
g.setColor(c.c);
g.setFont(new Font(fname, c.style, fsize));
Segment segm = getLineBuffer();
doc.getText(p0+curr, 1, segm);
x = Utilities.drawTabbedText(segm, x, y, g, this, p0+curr);
}
g.setColor(Color.black);
g.setFont(new Font(fname, Font.PLAIN, fsize));
}
catch(BadLocationException ex)
{
//System.out.println("ex = "+ex);
//ex.printStackTrace();
}
return x;
}
protected int drawSelectedText(Graphics g, int x, int y,int p0, int p1) throws BadLocationException
{
int stLine = findStartOfLine(p0, getDocument());
int enLine = findEndOfLine(p1, getDocument());
if (g instanceof Graphics2D) {
Graphics2D g2d = (Graphics2D)g;
g2d.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING, RenderingHints.VALUE_TEXT_ANTIALIAS_ON);
}
try
{
g.setColor(Color.green);
Document doc = getDocument();
Segment segment = getLineBuffer();
//String s = doc.getText(p0, p1-p0);
String s = doc.getText(stLine, enLine-stLine);
userinterface.model.Style[] styles = highlight(s, (p0-stLine), (p1-p0));
int currStart = 0;
int currEnd = 0;
Color last = null;
String fname = handler.getPepaEditorFontFast().getName();
int fsize = handler.getPepaEditorFontFast().getSize();
for(int curr = 0; curr < styles.length; curr++)
{
userinterface.model.Style c = styles[curr];
g.setColor(c.c);
g.setFont(new Font(fname, c.style, fsize));
Segment segm = getLineBuffer();
doc.getText(p0+curr, 1, segm);
x = Utilities.drawTabbedText(segm, x, y, g, this, p0+curr);
}
g.setColor(Color.black);
g.setFont(new Font(fname, Font.PLAIN, fsize));
}
catch(BadLocationException ex)
{
//System.out.println("ex = "+ex);
//ex.printStackTrace();
}
return x;
}
private synchronized userinterface.model.Style[] highlight(String s, int offset, int length)
{
userinterface.model.Style[] styles = new userinterface.model.Style[s.length()];
for(int i = 0; i < styles.length; i++)
styles[i] = PLAIN_S;
match = pattern.matcher(s);
int starter = 0;
int end = 0;
boolean contain = match.find();
while(contain)
{
starter = match.start();
end = match.end();
for(int j = starter; j < end; j++)
{
styles[j] = handler.getPepaEditorCommentFast();
}
contain = match.find();
}
//System.out.println("styles.length = "+styles.length);
//System.out.println("ret.length = "+length);
//System.out.println("offset = "+offset);
userinterface.model.Style[]ret = new userinterface.model.Style[length];
for(int i = 0; i < ret.length; i++)
{
ret[i] = styles[i+offset];
}
return ret;
}
private synchronized int findStartOfLine(int p0, Document d)
{
int index = p0;
String s = "";
try
{
s = d.getText(index, 1);
}
catch(BadLocationException e)
{
return 0;
}
index--;
if(!(!s.equals("\n") && index >= -1)) index--;//botch of the century, an alternative good code
while(!s.equals("\n") && index >= -1)
{
try
{
s = d.getText(index, 1);
}
catch(BadLocationException e)
{
return 0;
}
index--;
}
index+=2;
return index;
}
private synchronized int findEndOfLine(int p1, Document d)
{
int index = p1;
String s = "";
try
{
s = d.getText(index, 1);
}
catch(BadLocationException e)
{
return d.getLength();
}
index++;
while(!s.equals("\n") && index <= d.getLength())
{
try
{
s = d.getText(index, 1);
}
catch(BadLocationException e)
{
return d.getLength()-1;
}
index++;
}
index--;
return index;
}
}
}
You can’t perform that action at this time.