01: /*******************************************************************************
02: * Copyright (c) 2000, 2005 IBM Corporation and others.
03: * All rights reserved. This program and the accompanying materials
04: * are made available under the terms of the Eclipse Public License v1.0
05: * which accompanies this distribution, and is available at
06: * http://www.eclipse.org/legal/epl-v10.html
07: *
08: * Contributors:
09: * IBM Corporation - initial API and implementation
10: *******************************************************************************/package org.eclipse.ui.texteditor;
11:
12: import org.eclipse.jface.text.BadLocationException;
13: import org.eclipse.jface.text.IDocument;
14: import org.eclipse.jface.text.Position;
15:
16: import org.eclipse.core.resources.IMarker;
17:
18: /**
19: * Updates a marker's positional attributes which are
20: * start position, end position, and line number.
21: */
22: public final class BasicMarkerUpdater implements IMarkerUpdater {
23:
24: private final static String[] ATTRIBUTES = { IMarker.CHAR_START,
25: IMarker.CHAR_END, IMarker.LINE_NUMBER };
26:
27: /**
28: * Creates a new basic marker updater.
29: */
30: public BasicMarkerUpdater() {
31: super ();
32: }
33:
34: /*
35: * @see IMarkerUpdater#getAttribute()
36: */
37: public String[] getAttribute() {
38: return ATTRIBUTES;
39: }
40:
41: /*
42: * @see IMarkerUpdater#getMarkerType()
43: */
44: public String getMarkerType() {
45: return null;
46: }
47:
48: /*
49: * @see IMarkerUpdater#updateMarker(IMarker, IDocument, Position)
50: */
51: public boolean updateMarker(IMarker marker, IDocument document,
52: Position position) {
53:
54: if (position == null)
55: return true;
56:
57: if (position.isDeleted())
58: return false;
59:
60: boolean offsetsInitialized = false;
61: boolean offsetsChanged = false;
62: int markerStart = MarkerUtilities.getCharStart(marker);
63: int markerEnd = MarkerUtilities.getCharEnd(marker);
64:
65: if (markerStart != -1 && markerEnd != -1) {
66:
67: offsetsInitialized = true;
68:
69: int offset = position.getOffset();
70: if (markerStart != offset) {
71: MarkerUtilities.setCharStart(marker, offset);
72: offsetsChanged = true;
73: }
74:
75: offset += position.getLength();
76: if (markerEnd != offset) {
77: MarkerUtilities.setCharEnd(marker, offset);
78: offsetsChanged = true;
79: }
80: }
81:
82: if (!offsetsInitialized
83: || (offsetsChanged && MarkerUtilities
84: .getLineNumber(marker) != -1)) {
85: try {
86: // marker line numbers are 1-based
87: MarkerUtilities.setLineNumber(marker, document
88: .getLineOfOffset(position.getOffset()) + 1);
89: } catch (BadLocationException x) {
90: }
91: }
92:
93: return true;
94: }
95: }
|