001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.java;
012:
013: import java.io.IOException;
014: import java.io.StringWriter;
015:
016: import de.uka.ilkd.key.util.ExtList;
017:
018: /**
019: * Top level implementation of a Java {@link SourceElement}.
020: * taken from COMPOST and changed to achieve an immutable structure
021: */
022: public abstract class JavaSourceElement implements SourceElement {
023:
024: private final PositionInfo posInfo;
025:
026: /**
027: * Java source element.
028: */
029: public JavaSourceElement() {
030: posInfo = PositionInfo.UNDEFINED;
031: }
032:
033: /**
034: * Java source element.
035: * @param pi PositionInfo the PositionInfo of the element
036: */
037: public JavaSourceElement(PositionInfo pi) {
038: posInfo = getPosInfo(pi);
039: }
040:
041: /**
042: * Java source element.
043: * @param children a list of the children of this element. May contain:
044: * PositionInfo
045: */
046: public JavaSourceElement(ExtList children) {
047: posInfo = getPosInfo((PositionInfo) children
048: .get(PositionInfo.class));
049:
050: }
051:
052: public JavaSourceElement(ExtList children, PositionInfo pos) {
053: posInfo = getPosInfo(pos);
054: }
055:
056: /**
057: * internal method use to guarantee the position info object is
058: * always not the null reference
059: * @param p a PositionInfo
060: * @return if <tt>p</tt> is <tt>null</tt> the undefined
061: * position ({@link PositionInfo#UNDEFINED}) is returned otherwise
062: * <tt>p</tt>
063: */
064: private PositionInfo getPosInfo(PositionInfo p) {
065: final PositionInfo pos;
066: if (p == null) {
067: pos = PositionInfo.UNDEFINED;
068: } else {
069: pos = p;
070: }
071: return pos;
072: }
073:
074: /**
075: * Finds the source element that occurs first in the source. The default
076: * implementation returns this element, which is correct for all terminal
077: * program elements, and many non terminals such as statements and prefixed
078: * operators.
079: * @return the first source element in the syntactical representation of
080: * this element, may be equals to this element.
081: * @see #toSource()
082: * @see #getStartPosition()
083: */
084:
085: public SourceElement getFirstElement() {
086: return this ;
087: }
088:
089: /**
090: * Finds the source element that occurs last in the source. The
091: * default implementation returns this element, which is correct
092: * for all terminal program elements, and many non terminals such
093: * as statements and prefixed operators.
094: * @return the last source element in the syntactical representation of
095: * this element, may be equals to this element.
096: * @see #toSource()
097: * @see #getEndPosition()
098: */
099:
100: public SourceElement getLastElement() {
101: return this ;
102: }
103:
104: /**
105: * Pretty printing the source element.
106: */
107:
108: public abstract void prettyPrint(PrettyPrinter w)
109: throws IOException;
110:
111: /**
112: * Creates a syntactical representation of the source element using
113: * the {@link #prettyPrint} method.
114: */
115:
116: public String toSource() {
117: return toString();
118: }
119:
120: /**
121: Returns the start position of the primary token of this element.
122: To get the start position of the syntactical first token,
123: call the corresponding method of <CODE>getFirstElement()</CODE>.
124: @return the start position of the primary token.
125: */
126: public Position getStartPosition() {
127: return posInfo.getStartPosition();
128: }
129:
130: /**
131: Returns the end position of the primary token of this element.
132: To get the end position of the syntactical first token,
133: call the corresponding method of <CODE>getLastElement()</CODE>.
134: @return the end position of the primary token.
135: */
136: public Position getEndPosition() {
137: return posInfo.getEndPosition();
138: }
139:
140: /**
141: Returns the relative position (number of blank heading lines and
142: columns) of the primary token of this element.
143: To get the relative position of the syntactical first token,
144: call the corresponding method of <CODE>getFirstElement()</CODE>.
145: @return the relative position of the primary token.
146: */
147: public Position getRelativePosition() {
148: return posInfo.getRelativePosition();
149: }
150:
151: public PositionInfo getPositionInfo() {
152: return posInfo;
153: }
154:
155: /** toString */
156: public String toString() {
157: StringWriter sw = new StringWriter();
158: try {
159: PrettyPrinter pp = new PrettyPrinter(sw, true);
160: pp.setIndentationLevel(0);
161: prettyPrint(pp);
162: } catch (IOException e) {
163: System.err
164: .println("Pretty printing of JavaSourceElemet failed");
165: System.err.println("Due to " + e);
166: e.printStackTrace();
167: }
168: String r = sw.toString();
169: r = r.replace('\n', ' ');
170: r = r.replace('\t', ' ');
171: return r;
172: }
173:
174: /** this violates immutability, but the method is only called
175: * right after the object is created...
176: */
177: protected void setParentClass(String s) {
178: posInfo.setParentClass(s);
179: }
180:
181: /** get the class the statement originates from */
182: public String getParentClass() {
183: return posInfo.getParentClass();
184: }
185:
186: }
|