001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.gui.se.pane;
017
018 import java.awt.BorderLayout;
019 import java.awt.event.MouseEvent;
020 import java.io.IOException;
021 import java.util.List;
022
023 import javax.swing.BorderFactory;
024 import javax.swing.JPanel;
025 import javax.swing.JScrollPane;
026 import javax.swing.JTextArea;
027 import javax.swing.JViewport;
028 import javax.swing.SwingUtilities;
029 import javax.swing.UIManager;
030 import javax.swing.plaf.TextUI;
031 import javax.swing.text.BadLocationException;
032
033 import org.qedeq.base.io.SourceArea;
034 import org.qedeq.base.trace.Trace;
035 import org.qedeq.base.utility.EqualsUtility;
036 import org.qedeq.gui.se.control.SelectionListener;
037 import org.qedeq.gui.se.element.CPTextArea;
038 import org.qedeq.gui.se.util.CurrentLineHighlighterUtility;
039 import org.qedeq.gui.se.util.DocumentMarker;
040 import org.qedeq.gui.se.util.DocumentMarkerPainter;
041 import org.qedeq.gui.se.util.GuiHelper;
042 import org.qedeq.kernel.bo.KernelContext;
043 import org.qedeq.kernel.bo.common.QedeqBo;
044 import org.qedeq.kernel.se.common.SourceFileException;
045 import org.qedeq.kernel.se.common.SourceFileExceptionList;
046
047 /**
048 * View source of QEDEQ module.
049 *
050 * @author Michael Meyling
051 */
052
053 public class QedeqPane extends JPanel implements SelectionListener {
054
055 /** This class. */
056 private static final Class CLASS = QedeqPane.class;
057
058 /** Reference to module properties. */
059 private QedeqBo prop;
060
061 /** Here is the QEDEQ module source. */
062 private JTextArea qedeq = new CPTextArea(false) {
063 public String getToolTipText(final MouseEvent e) {
064 if (errorMarker == null || warningMarker == null) {
065 setToolTipText(null);
066 return super.getToolTipText();
067 }
068 // --- determine locations ---
069 TextUI mapper = qedeq.getUI();
070 final int i = mapper.viewToModel(qedeq, e.getPoint());
071 final List errNos = errorMarker.getBlockNumbersForOffset(i);
072 final List warningNos = warningMarker.getBlockNumbersForOffset(i);
073 if (errNos.size() == 0 && warningNos.size() == 0) {
074 setToolTipText(null);
075 return super.getToolTipText(e);
076 }
077 final StringBuffer buffer = new StringBuffer();
078 buffer.append("<html>");
079 for (int j = 0; j < errNos.size(); j++) {
080 if (j > 0) {
081 buffer.append("<br>");
082 }
083 buffer.append((prop.getErrors().get(((Integer) errNos.get(j)).intValue())
084 .getMessage())); // TODO mime 20080417: escape for HTML presenatation
085 }
086 for (int j = 0; j < warningNos.size(); j++) {
087 if (j > 0) {
088 buffer.append("<br>");
089 }
090 buffer.append((prop.getWarnings().get(((Integer) warningNos.get(j)).intValue())
091 .getMessage())); // TODO mime 20080417: escape for HTML presenatation
092 }
093 buffer.append("</html>");
094 setToolTipText(buffer.toString());
095 return getToolTipText();
096 }
097 };
098
099 /** Our error highlighter for the text areas. */
100 private DocumentMarker errorMarker;
101
102 /** Our warning highlighter for the text areas. */
103 private DocumentMarker warningMarker;
104
105 /**
106 * Creates new Panel.
107 */
108 public QedeqPane() {
109 super(false);
110 this.prop = null;
111 setupView();
112 updateView();
113 }
114
115 /**
116 * Assembles the GUI components of the panel.
117 */
118 public void setupView() {
119 final JScrollPane scroller = new JScrollPane();
120 final JViewport vp = scroller.getViewport();
121 vp.add(qedeq);
122 this.setLayout(new BorderLayout(0, 0));
123 this.add(scroller);
124 setBorder(BorderFactory.createEmptyBorder());
125 qedeq.setEditable(false);
126 qedeq.setToolTipText("");
127 qedeq.putClientProperty("JTextArea.infoBackground", Boolean.TRUE);
128 qedeq.setLineWrap(true); // TODO mime 20080509: make this configurable
129 }
130
131 /**
132 * Set new model. To make the new model visible {@link #updateView} must be called.
133 *
134 * @param prop New QEDEQ module.
135 */
136 public synchronized void setModel(final QedeqBo prop) {
137 Trace.trace(CLASS, this, "setModel", prop);
138 if (!EqualsUtility.equals(this.prop, prop)) {
139 this.prop = prop;
140 Runnable setModel = new Runnable() {
141 public void run() {
142 updateView();
143 }
144 };
145 SwingUtilities.invokeLater(setModel);
146 }
147 }
148
149
150 public void setLineWrap(final boolean wrap) {
151 qedeq.setLineWrap(wrap);
152 }
153
154 public boolean getLineWrap() {
155 return qedeq.getLineWrap();
156 }
157
158 /**
159 * Update from model.
160 */
161 public synchronized void updateView() {
162 Trace.begin(CLASS, this, "updateView");
163 if (prop != null) {
164 try {
165 qedeq.setText(KernelContext.getInstance().getSource(prop.getModuleAddress()));
166 CurrentLineHighlighterUtility.install(qedeq);
167 qedeq.setLineWrap(getLineWrap());
168 if (prop.getModuleAddress().isFileAddress()) {
169 qedeq.setEditable(true);
170 } else {
171 // TODO 20100319 m31: show "readonly" as label somewhere
172 qedeq.setEditable(false);
173 }
174 // we want the background be same even if area is not editable
175 qedeq.setBackground(UIManager.getColor("TextArea.background"));
176 qedeq.setCaretPosition(0);
177 qedeq.getCaret().setSelectionVisible(true);
178
179 // TODO m31 20100707: duplicate code, refactor
180 warningMarker = new DocumentMarker(qedeq, new DocumentMarkerPainter(
181 GuiHelper.getWarningTextBackgroundColor()));
182 final SourceFileExceptionList pw = prop.getWarnings();
183 if (pw != null) {
184 for (int i = 0; i < pw.size(); i++) {
185 if (pw.get(i).getSourceArea() != null) {
186 try {
187 final SourceArea sa = pw.get(i).getSourceArea();
188 if (sa != null) {
189 final int from = sa.getStartPosition().getRow() - 1;
190 int to = sa.getEndPosition().getRow() - 1;
191 // for line marking only:
192 // warningMarker.addWarningLines(from, to,
193 // sa.getStartPosition().getColumn() - 1);
194 warningMarker.addMarkedBlock(from,
195 sa.getStartPosition().getColumn() - 1,
196 to, sa.getEndPosition().getColumn() - 1);
197 continue;
198 }
199 } catch (BadLocationException e) { // should not occur
200 Trace.fatal(CLASS, this, "updateView", "Programming error?", e);
201 }
202 } else {
203 warningMarker.addEmptyBlock();
204 }
205 }
206 }
207 errorMarker = new DocumentMarker(qedeq, new DocumentMarkerPainter(
208 GuiHelper.getErrorTextBackgroundColor()));
209 final SourceFileExceptionList pe = prop.getErrors();
210 if (pe != null) {
211 for (int i = 0; i < pe.size(); i++) {
212 if (pe.get(i).getSourceArea() != null) {
213 try {
214 final SourceArea sa = pe.get(i).getSourceArea();
215 if (sa != null) {
216 final int from = sa.getStartPosition().getRow() - 1;
217 int to = sa.getEndPosition().getRow() - 1;
218 // for line marking only:
219 // errorMarker.addMarkedLines(from, to,
220 // sa.getStartPosition().getColumn() - 1);
221 errorMarker.addMarkedBlock(from,
222 sa.getStartPosition().getColumn() - 1,
223 to, sa.getEndPosition().getColumn() - 1);
224 continue;
225 }
226 } catch (BadLocationException e) { // should not occur
227 Trace.fatal(CLASS, this, "updateView", "Programming error?", e);
228 }
229 } else {
230 errorMarker.addEmptyBlock();
231 }
232 }
233 }
234 Trace.trace(CLASS, this, "updateView", "Text updated");
235 } catch (IOException ioException) {
236 qedeq.setEditable(false);
237 qedeq.setText("");
238 Trace.trace(CLASS, this, "updateView", ioException);
239 }
240 } else {
241 errorMarker = null;
242 warningMarker = null;
243 CurrentLineHighlighterUtility.uninstall(qedeq);
244 qedeq.setEditable(false);
245 qedeq.setText("");
246 Trace.end(CLASS, this, "updateView");
247 }
248 this.repaint();
249 }
250
251
252 /**
253 * Get QEDEQ text, if QEDEQ text is editable.
254 *
255 * @return QEDEQ text source.
256 * @throws IllegalStateException QEDEQ text is not editable.
257 */
258 public final String getEditedQedeq() {
259 if (qedeq.isEditable()) {
260 return this.qedeq.getText();
261 } else {
262 throw new IllegalStateException("no editable QEDEQ text");
263 }
264 }
265
266
267 /**
268 * Was the content changed?
269 *
270 * @return content modified?
271 */
272 public final boolean isContentChanged() {
273 return !this.qedeq.isEditable();
274 }
275
276
277 // LATER m31 20100830: not used any longer
278 /*
279 private final int findCaretPosition(final int i) {
280 if (i == 1) {
281 return 0;
282 }
283 final String s = qedeq.getText();
284 int j = 0;
285 int k = 0;
286 for (; j < s.length(); j++) {
287 if (s.charAt(j) == '\n') {
288 k++;
289 }
290 if (k == i - 1) {
291 return j + 1;
292 }
293 }
294 return 0;
295 }
296
297 private final void highlightLine(final int line) {
298 Trace.param(CLASS, this, "highlightLine", "line", line);
299 int j;
300 try {
301 j = qedeq.getLineStartOffset(line - 1);
302 } catch (BadLocationException e) {
303 Trace.trace(CLASS, this, "highlightLine", e);
304 j = 0;
305 }
306 int k;
307 try {
308 k = qedeq.getLineEndOffset(line - 1);
309 } catch (BadLocationException e) {
310 Trace.trace(CLASS, this, "highlightLine", e);
311 k = qedeq.getText().length();
312 }
313 Trace.trace(CLASS, this, "highlightLine", "from " + j + " to " + k);
314
315 qedeq.setCaretPosition(j);
316 qedeq.moveCaretPosition(k);
317 }
318
319 // public void selectError(final int number) {
320 // if (prop != null && prop.getException() != null && number < prop.getException().size()) {
321 // final SourceFileException sfe = prop.getException().get(number);
322 // if (sfe.getSourceArea() != null && sfe.getSourceArea().getStartPosition() != null) {
323 // highlightLine(sfe.getSourceArea().getStartPosition().getLine());
324 // }
325 // }
326 // }
327 */
328
329 /**
330 * Jump to error location. Uses only <code>error</code> to select correct marker.
331 *
332 * @param error Selected error number. Starts with 0.
333 * @param sf Selected error.
334 */
335 public synchronized void selectError(final int error, final SourceFileException sf) {
336 if (errorMarker != null) {
337 this.requestFocus();
338 qedeq.requestFocus();
339 qedeq.setCaretPosition(errorMarker.getLandmarkOffsetForBlock(error));
340 } else {
341 Trace.paramInfo(CLASS, "selectError", "errorMarker", "null");
342 }
343 }
344
345 /**
346 * Jump to warning location. Uses only <code>warning</code> to select correct marker.
347 *
348 * @param warning Selected warning number. Starts with 0.
349 * @param sf Selected warning.
350 */
351 public synchronized void selectWarning(final int warning, final SourceFileException sf) {
352 int block = warning;
353 // if (prop != null && prop.getErrors().size() > 0) {
354 // block += prop.getErrors().size();
355 // }
356 if (warningMarker != null) {
357 this.requestFocus();
358 qedeq.requestFocus();
359 qedeq.setCaretPosition(warningMarker.getLandmarkOffsetForBlock(block));
360 } else {
361 Trace.paramInfo(CLASS, "selectWarning", "warningMarker", "null");
362 }
363 }
364
365 }
|