001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * The main author is Santhosh Kumar T. Visit his great home page under:
004 * http://www.jroller.com/santhosh/
005 *
006 * The original source for this file is:
007 * http://www.jroller.com/santhosh/entry/document_guard
008 *
009 * It is distributed under the GNU Lesser General Public License:
010 * http://www.gnu.org/copyleft/lesser.html
011 */
012
013 package org.qedeq.gui.se.util;
014
015 import java.util.ArrayList;
016 import java.util.List;
017
018 import javax.swing.JTextArea;
019 import javax.swing.text.AbstractDocument;
020 import javax.swing.text.BadLocationException;
021 import javax.swing.text.Highlighter;
022 import javax.swing.text.Position;
023
024 /**
025 * Mark text areas (aka blocks) in another background color. Precondition is an installed
026 * {@link org.qedeq.gui.se.util.CurrentLineHighlighterUtility}.
027 *
028 * @author Santhosh Kumar T
029 * @author Michael Meyling
030 */
031 public class DocumentMarker {
032
033 /** We mark areas in this text component. */
034 private JTextArea textComp;
035
036 /** Our highlighter for the text areas. */
037 private Highlighter.HighlightPainter highlightPainter;
038
039
040 /** Contains all positions. Each entry is of type {@link Position}[3]. The first position is
041 * the starting offset, second is the end offset and third is the landmark position. It is
042 * also possible that we have an empty block, that situation is represented by a
043 * <code>null</code> entry in the list. */
044 private final List pos = new ArrayList();
045
046 /**
047 * Constructor.
048 *
049 * @param textComp Text Component with marked areas.
050 * @param highlightPainter Our highlighter.
051 */
052 public DocumentMarker(final JTextArea textComp, final Highlighter.HighlightPainter highlightPainter) {
053 this.textComp = textComp;
054 this.highlightPainter = highlightPainter;
055 }
056
057 public int getOffsetOfFistLineFromBlock(final int blockNumber) {
058 int offset = 0;
059 if (0 <= blockNumber && blockNumber < pos.size()) {
060 Position[] p = (Position[]) pos.get(blockNumber);
061 if (p != null) { // no empty block?
062 offset = p[0].getOffset();
063 }
064 }
065 return offset;
066 }
067
068 /**
069 * Get offset for landmark position of block.
070 *
071 * @param blockNumber Get landmark for this block.
072 * @return Offset for this landmark.
073 */
074 public int getLandmarkOffsetForBlock(final int blockNumber) {
075 int offset = 0;
076 if (0 <= blockNumber && blockNumber < pos.size()) {
077 Position[] p = (Position[]) pos.get(blockNumber);
078 if (p != null) { // no empty block?
079 offset = p[2].getOffset();
080 }
081 }
082 return offset;
083 }
084
085 public List getBlockNumbersForOffset(final int offset) {
086 List list = new ArrayList();
087 for (int i = 0; i < pos.size(); i++) {
088 Position[] p = (Position[]) pos.get(i);
089 if (p == null) { // empty block?
090 continue;
091 }
092 int g1 = p[0].getOffset() - 1, g2 = p[1].getOffset() + 1;
093 if (g1 < offset && offset < g2) {
094 list.add(new Integer(i));
095 }
096 }
097 return list;
098 }
099
100 /**
101 * Add an empty block. This is useful for representing errors that have no specific location.
102 * (Another solution might be a block from offset 0 to 0.)
103 */
104 public void addEmptyBlock() {
105 pos.add(null);
106 }
107
108 public void addMarkedLines(final int fromLine, final int toLine, final int off)
109 throws BadLocationException {
110 int fromOffset = textComp.getLineStartOffset(fromLine);
111 int toOffset = textComp.getLineEndOffset(toLine);
112 addMarkedBlock(fromOffset, toOffset, fromOffset + off);
113 }
114
115 public void addMarkedBlock(final int startLine, final int startLineOffset, final int endLine,
116 final int endLineOffset) throws BadLocationException {
117 AbstractDocument doc = (AbstractDocument) textComp.getDocument();
118 int fromOffset = textComp.getLineStartOffset(startLine) + startLineOffset;
119 int toOffset = textComp.getLineStartOffset(endLine) + endLineOffset;
120 addMarkedBlock(doc.createPosition(fromOffset), doc.createPosition(toOffset - 1), doc
121 .createPosition(fromOffset));
122 textComp.getHighlighter().addHighlight(fromOffset + 1, toOffset - 1, highlightPainter);
123 }
124
125 private void addMarkedBlock(final int fromOffset, final int toOffset, final int pos)
126 throws BadLocationException {
127 AbstractDocument doc = (AbstractDocument) textComp.getDocument();
128 addMarkedBlock(doc.createPosition(fromOffset), doc.createPosition(toOffset - 1), doc
129 .createPosition(pos));
130 textComp.getHighlighter().addHighlight(fromOffset + 1, toOffset - 1, highlightPainter);
131 }
132
133 private void addMarkedBlock(final Position start, final Position end, final Position pos)
134 throws BadLocationException {
135 this.pos.add(new Position[] {start, end, pos});
136 }
137
138 }
|