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: package de.uka.ilkd.key.util.pp;
011:
012: import java.io.IOException;
013: import java.util.ArrayList;
014:
015: /** The intermediate layer of the pretty printing library. Using the
016: * block size information provided by the {@link Layouter} class, this
017: * decides where to insert line breaks. It tries to break as few
018: * blocks as possible. */
019:
020: class Printer {
021:
022: /** Mask for break type flags. These flags are logically or-ed
023: * onto the margins in the marginStack to remember what happens
024: * with the block in question. */
025: private static final int BREAK_MASK = 0x70000000;
026: /** Flag to indicate this block fits into the current line */
027: private static final int FITS = 0x00000000;
028: /** Flag to indicate this block will be broken consistently */
029: private static final int CONSISTENT = 0x10000000;
030: /** Flag to indicate this block will be broken inconsistently */
031: private static final int INCONSISTENT = 0x20000000;
032:
033: /** total line length available */
034: private final int lineWidth;
035:
036: /** position in current line. */
037: private int pos;
038:
039: /** total chars written */
040: private int totalOut = 0;
041:
042: /** Back-end for the pretty-printed output */
043: private Backend back;
044:
045: /** stack to remember value of <code>pos</code> in nested blocks */
046: private ArrayList marginStack = new ArrayList(10);
047:
048: /** Create a printer. It will write its output to <code>writer</code>.
049: * Lines have a maximum width of <code>lineWidth</code>. */
050: Printer(Backend back) {
051: this .back = back;
052: lineWidth = back.lineWidth();
053: pos = 0;
054: }
055:
056: /** write the String <code>s</code> to <code>out</code> */
057: void print(String s) throws IOException {
058: back.print(s);
059: pos += back.measure(s);
060: totalOut += back.measure(s);
061: }
062:
063: /** begin a block */
064: void openBlock(boolean consistent, int indent, int followingLength) {
065: if (followingLength + pos > lineWidth) {
066: push(pos + indent, consistent ? CONSISTENT : INCONSISTENT);
067: } else {
068: push(0, FITS);
069: }
070: }
071:
072: /** end a block */
073: void closeBlock() {
074: pop();
075: }
076:
077: /**
078: * write a break. <code>followingLength</code> should be the
079: * space needed by the material up to the next corresponding
080: * closeBlock() or printBreak(), and is used to decide whether the
081: * current line is continues, or a new (indented) line is begun.
082: * */
083: void printBreak(int width, int offset, int followingLength)
084: throws IOException {
085:
086: if (topBreak() == CONSISTENT
087: || (topBreak() == INCONSISTENT && followingLength > (lineWidth - pos))) {
088:
089: pos = topMargin() + offset;
090:
091: newLine();
092: } else {
093: writeSpaces(width);
094: pos += width;
095: }
096: }
097:
098: void mark(Object o) {
099: back.mark(o);
100: }
101:
102: void indent(int width, int offset) throws IOException {
103: int newMargin = topMargin() + offset;
104: if (topBreak() != FITS) {
105: if (newMargin > pos) {
106: writeSpaces(newMargin - pos);
107: pos = newMargin;
108: }
109: } else {
110: writeSpaces(width);
111: pos += width;
112: }
113: }
114:
115: /** Close the output stream. */
116: void close() throws IOException {
117: back.close();
118: }
119:
120: /** Flush the output stream. */
121: void flush() throws IOException {
122: back.flush();
123: }
124:
125: /** Return the amount of space currently left on this line. */
126: int space() {
127: return lineWidth - pos;
128: }
129:
130: /** Return the line width of this Printer. */
131: int lineWidth() {
132: return lineWidth;
133: }
134:
135: private void push(int n, int breaks) {
136: marginStack.add(new Integer(n | breaks));
137: }
138:
139: /** Pop one element from the space stack. */
140: private void pop() {
141: try {
142: marginStack.remove(marginStack.size() - 1);
143: } catch (IndexOutOfBoundsException e) {
144: throw new UnbalancedBlocksException();
145: }
146: }
147:
148: /** return the topmost element of the space stack without popping it. */
149: private int top() {
150: try {
151: return ((Integer) marginStack.get(marginStack.size() - 1))
152: .intValue();
153: } catch (IndexOutOfBoundsException e) {
154: throw new UnbalancedBlocksException();
155: }
156: }
157:
158: private int topMargin() {
159: return top() & ~BREAK_MASK;
160: }
161:
162: private int topBreak() {
163: return top() & BREAK_MASK;
164: }
165:
166: /** Start a new line and indent according to <code>pos</code>
167: */
168: private void newLine() throws IOException {
169: back.newLine();
170: totalOut++;
171: if (pos > 0) {
172: writeSpaces(pos);
173: }
174: }
175:
176: /** how many spaces */
177: private static final int SPACES = 128;
178:
179: /** a String containing <code>SPACES</code> spaces */
180: private static final String spaces;
181:
182: /* initialize spaces */
183: static {
184: StringBuffer sb = new StringBuffer(SPACES);
185: for (int i = 0; i < SPACES; i++) {
186: sb.append(' ');
187: }
188: spaces = sb.toString();
189: }
190:
191: private void writeSpaces(int n) throws IOException {
192: while (n > SPACES) {
193: back.print(spaces);
194: n -= SPACES;
195: }
196: back.print(spaces.substring(0, n));
197: totalOut += n;
198: }
199: }
|