001 package nl.cwi.sen1.gui.plugin.editor;
002
003 import java.awt.BorderLayout;
004 import java.awt.Point;
005 import java.awt.event.MouseListener;
006 import java.io.BufferedInputStream;
007 import java.io.BufferedOutputStream;
008 import java.io.File;
009 import java.io.FileInputStream;
010 import java.io.FileNotFoundException;
011 import java.io.FileOutputStream;
012 import java.io.IOException;
013 import java.io.InputStream;
014 import java.io.OutputStream;
015
016 import javax.swing.JMenu;
017 import javax.swing.JPanel;
018 import javax.swing.JScrollPane;
019
020 import nl.cwi.sen1.configapi.types.PropertyList;
021 import nl.cwi.sen1.gui.plugin.Editor;
022 import nl.cwi.sen1.gui.plugin.EditorModifiedListener;
023 import aterm.ATerm;
024 import aterm.ATermList;
025 import errorapi.types.Area;
026
027 public class SwingEditor extends JPanel implements Editor {
028 private String id;
029
030 private String filename;
031
032 private EditorPane editorPane;
033
034 public SwingEditor(String id, String filename) throws IOException,
035 FileToBigException {
036 this.id = id;
037 this.filename = filename;
038
039 setLayout(new BorderLayout());
040 editorPane = new EditorPane();
041
042 readFileContents();
043 editorPane.setCaretPosition(0);
044
045 JScrollPane scroller = new JScrollPane(editorPane);
046
047 add(scroller, BorderLayout.CENTER);
048 }
049
050 public void rereadContents() {
051 try {
052 readFileContents();
053 // ((EditorKit) editorPane.getEditorKit()).getUndoManager()
054 // .discardAllEdits();
055 } catch (IOException e) {
056 e.printStackTrace();
057 } catch (FileToBigException e) {
058 e.printStackTrace();
059 }
060 }
061
062 private void readFileContents() throws IOException,
063 FileToBigException {
064 editorPane.setText(readContents());
065 }
066
067 private String readContents() throws IOException,
068 FileToBigException {
069 InputStream fis = null;
070
071 try {
072 File file = new File(filename);
073 fis = new BufferedInputStream(new FileInputStream(filename));
074 long x = file.length();
075
076 if (x > 1024 * 1024 /* 1 Mbyte */) {
077 throw new FileToBigException(filename);
078 }
079
080 byte b[] = new byte[(int) x];
081 fis.read(b);
082 String content = new String(b);
083 return content;
084 } catch (FileNotFoundException e) {
085 return "";
086 } finally {
087 if (fis != null) {
088 fis.close();
089 }
090 }
091 }
092
093 public String getContents() {
094 return editorPane.getText();
095 }
096
097 public void setContents(String contents) {
098 editorPane.setText(contents);
099 }
100
101 public void writeContents(String filename) throws IOException {
102 String text = editorPane.getText();
103
104 OutputStream fos = null;
105 try{
106 fos = new BufferedOutputStream(new FileOutputStream(filename));
107 fos.write(text.getBytes());
108 }finally{
109 if(fos != null){
110 fos.close();
111 }
112 }
113
114 editorPane.setModified(false);
115 editorPane.clearJaggedSelection();
116 }
117
118 public void writeCopy(String filename) throws IOException {
119 String text = editorPane.getText();
120
121 FileOutputStream fos = null;
122 try{
123 fos = new FileOutputStream(filename);
124 fos.write(text.getBytes());
125 }finally{
126 if(fos != null){
127 fos.close();
128 }
129 }
130 }
131
132 public void setCursorAtOffset(int offset) {
133 try {
134 editorPane.setCaretPosition(offset);
135 } catch (IllegalArgumentException e) {
136 editorPane.setCaretPositionAtEnd();
137 }
138 }
139
140 public void setFocus(Area focus) {
141 editorPane.focus(focus.getOffset(), focus.getOffset()
142 + focus.getLength());
143 }
144
145 public void setSelection(Area area) {
146 editorPane.jag(area.getOffset(), area.getOffset()
147 + area.getLength());
148 }
149
150 public String getId() {
151 return id;
152 }
153
154 public String getFilename() {
155 return filename;
156 }
157
158 public void setModified(boolean modified) {
159 editorPane.setModified(modified);
160 clearSelections();
161 }
162
163 public boolean isModified() {
164 return editorPane.isModified();
165 }
166
167 public void registerCategories(PropertyList properties) {
168 StyleRegistrar.registerTextCategories(editorPane, properties);
169 }
170
171 public void registerSlices(ATerm slices) {
172 if (((ATermList) slices).getLength() < 10000) {
173 SliceRegistrar.registerSlices(editorPane, (ATermList) slices);
174 } else {
175 System.err
176 .println("Ignoring syntax highlighting for safety (too big)");
177 }
178 }
179
180 public int getMouseOffset(int x, int y) {
181 return editorPane.viewToModel(new Point(x, y));
182 }
183
184 public JMenu getEditMenu() {
185 return editorPane.getEditorMenu();
186 }
187
188 public void requestFocus() {
189 editorPane.requestFocus();
190 }
191
192 public void addMouseListener(MouseListener l) {
193 editorPane.addMouseListener(l);
194 }
195
196 public void removeMouseListener(MouseListener l) {
197 editorPane.removeMouseListener(l);
198 }
199
200 public void addEditorModifiedListener(EditorModifiedListener l) {
201 editorPane.addEditorModifiedListener(l);
202 }
203
204 public void removeEditorModifiedListener(EditorModifiedListener l) {
205 editorPane.removeEditorModifiedListener(l);
206 }
207
208 public void setEditable(boolean b) {
209 editorPane.setEditable(b);
210 }
211
212 public boolean isEditable() {
213 return editorPane.isEditable();
214 }
215
216 public void clearSelections() {
217 editorPane.clearFocus();
218 editorPane.clearJaggedSelection();
219 }
220 }