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.List;
014: import java.util.StringTokenizer;
015:
016: /**
017: * This class pretty-prints information using line breaks and
018: * indentation. For instance, it can be used to print
019: * <pre>
020: * while (i>0) {
021: * i--;
022: * j++;
023: * }
024: * </pre>
025: * instead of
026: * <pre>
027: * while (i>0) { i
028: * --; j++;}
029: * </pre>
030: * if a maximum line width of 15 characters is chosen.
031: *
032: * <P>The formatted output is directed to a <em>backend</em> which
033: * might write it to an I/O stream, append it to the text of a GUI
034: * componenet or store it in a string. The {@link Backend} interface
035: * encapsulates the concept of backend. Apart from handling the
036: * output, the backend is also asked for the available line width and
037: * for the amount of space needed to print a string. This makes it
038: * possible to include e.g. HTML markup in the output which does not
039: * take up any space. There are two convenience implementations
040: * {@link WriterBackend} and {@link StringBackend}, which write the
041: * output to a {@link java.io.Writer}, resp. a
042: *
043: * {@link java.lang.String}.
044: *
045: * <P>The layouter internally keeps track of a current <em>indentation
046: * level</em>. Think of nicely indented Java source code. Then the
047: * indentation level at any point is the number of blank columns to be
048: * inserted at the begining of the next line if you inserted a line
049: * break. To increase the indentation level of parts of the text, the
050: * input to the layouter is separated into <em>blocks</em>. The
051: * indentation level changes when a block is begun, and it is reset to
052: * its previous value when a block is ended. Of course, blocks maybe
053: * nested.
054: *
055: * <P>In order to break text among several lines, the layouter needs
056: * to be told where line breaks are allowed. A <em>break</em> is a
057: * position in the text where there is either a line break (with
058: * appropriate indentation) or a number of spaces, if enough material
059: * fits in one line. In order to handle the indentation level
060: * properly, breaks should only occur inside blocks. There are in
061: * fact two kinds of blocks: <em>consistent</em> and
062: * <em>inconsistent</em> ones. In a consistent block, line are broken
063: * either at all or at none of the breaks. In an inconsistent block,
064: * as much material as possible is put on one line before it is
065: * broken.
066: *
067: * <P>Consider the program above. It should be printed either as
068: * <pre>
069: * while (i>0) { i--; j++; }
070: * </pre>
071: * or, if there is not enough space on the line, as
072: * <pre>
073: * while (i>0) {
074: * i--;
075: * j++;
076: * }
077: * </pre>
078: * Given a Layouter object <code>l</code>, we could say:
079: * <pre>
080: * l.begin(true,2).print("while (i>0) {").brk(1,0)
081: * .print("i--;").brk(1,0)
082: * .print("j++;").brk(1,-2)
083: * .print("{").end();
084: * </pre>
085: *
086: * The call to {@link #begin(boolean,int)} starts a consistent block,
087: * increasing the indentation level by 2. The {@link #print(String)}
088: * methods gives some actual text to be output. The call to {@link
089: * #brk(int,int)} inserts a break. The first argument means that one
090: * space should be printed at this position if the line is
091: * <em>not</em> broken. The second argument is an offset to be added
092: * to the indentation level for the next line, if the line <em>is</em>
093: * broken. The effect of this parameter can be seen in the call
094: * <code>brk(1,-2)</code>. The offset of <code>-2</code> outdents the
095: * last line by 2 positions, which aligns the closing brace with the
096: * <code>with</code>.
097: *
098: * <p>If the lines in a block are broken, one sometimes wants to insert
099: * spaces up to the current indentation level at a certain position
100: * without allowing a line break there. This can be done using the
101: * {@link #ind(int,int)} method. For instance, one wants to output either
102: * <pre>
103: * ...[Good and Bad and Ugly]...
104: * </pre>
105: * or
106: * <pre>
107: * ...[ Good
108: * and Bad
109: * and Ugly]...
110: * </pre>
111: *
112: * Note the four spaces required before <code>Good</code>. We do this
113: * by opening a block which sets the indentation level to the column where the <code>G</code> ends up and outdenting the lines with the <code>and</code>:
114: * <pre>
115: * l.print("...[").begin(true,4).ind(0,0).print("Good").brk(1,-4)
116: * .print("and ").print("Bad").brk(1,-4)
117: * .print("and ").print("Ugly").end().print("]...");
118: * </pre>
119: *
120: * Again, the first argument to {@link #ind(int,int)} is a number of
121: * spaces to print if the block we are in is printed on one line. The
122: * second argument is an offset to be added to the current indentation
123: * level to determine the column to which we should skip.
124: *
125: * <p>When all text has been sent to a Layouter and all blocks have been
126: * ended, the {@link #close()} method should be closed. This sends
127: * all pending output to the backend and invokes the {@link
128: * Backend#close()} method, which usually closes I/O streams, etc.
129: *
130: * <p>Some applications need to keep track of where certain parts of the
131: * input text end up in the output. For this purpose, the Layouter
132: * class provides the {@link #mark(Object)} method.
133: *
134: * <P>The public methods of this class may be divided into two
135: * categories: A small number of <em>primitive</em> methods, as
136: * described above, and a host of <em>convenience</em> methods which
137: * simplify calling the primitive ones for often-used arguments. For
138: * instance a call to {@link #beginC()} is shorthand for
139: * <code>begin(true,ind)</code>, where <code>ind</code> is the default
140: * indentation selected when the Layouter was constructed.
141: *
142: * <P>Most of the methods can throw an {@link UnbalancedBlocksException},
143: * which indicates that the sequence of method calls was illegal, i.e.
144: * more blocks were ended than begun, the Layouter is closed before all
145: * blocks are ended, a break occurs outside of any block, etc.
146: *
147: * <P>Also, most methods can throw an {@link java.io.IOException}.
148: * This only happens if a called method in the backend throws an
149: * IOException, in which case that exception is passed through to the
150: * caller of the Layouter method.
151: *
152: * @author Martin Giese
153: * @see Backend
154: * */
155:
156: /*
157: * Implementation note: The name of this class is actually a lie.
158: * What this class does is calculate the space needed by blocks and
159: * portions of blocks between breaks if they are to printed in a
160: * single line. The actual laying out, that is choosing whether to
161: * break line or not is done by a Printer object, which in turn sends
162: * its output to the Backend.
163: *
164: */
165:
166: public class Layouter {
167:
168: /** The backend */
169: private Backend back;
170:
171: /** The Printer used for output. */
172: private Printer out;
173:
174: /** The list of scanned tokens not yet output. */
175: private List stream = new java.util.LinkedList();
176:
177: /** A stack of <code>OpenBlockToken</code>s and
178: * <code>BreakToken</code>s in <code>stream</code>, waiting for
179: * their size to be determined.*/
180: private List delimStack = new java.util.LinkedList();
181:
182: /*
183: * Some Invariants:
184: *
185: * delimStack.isEmpty() implies stream.isEmpty()
186: *
187: * Any OpenBlockToken in stream is also on the demlimStack.
188: * The latest BreakToken of any open block in the stream is
189: * also on the delim stack.
190: *
191: */
192:
193: /** Total size of received strings and blanks, if they were
194: * printed in one line. The difference of this between two states
195: * says how much space would be needed to print the intervening
196: * stuff without line breaks. */
197: private int totalSize = 0;
198:
199: /** Total size of strings and blanks sent to the Printer <code>out</code>.
200: * Subtract this from <code>totalOutput</code> and you get the space
201: * needed to print what is still buffered in <code>stream</code> */
202: private int totalOutput = 0;
203:
204: /** The size assigned to things which are guaranteed not to fit on a
205: * line. For good measure, this is intitialized to twice the line
206: * width by the constructors. */
207: private int largeSize;
208:
209: /** A default indentation value used for blocks. */
210: private int defaultInd;
211:
212: // PRIMITIVE CONSTRUCTOR -------------------------------------------
213:
214: /**
215: * Construts a newly allocated Layouter which will send output to
216: * the given {@link Backend} and has the given default indentation.
217: *
218: * @param backend the Backend
219: * @param indentation the default indentation
220: *
221: */
222:
223: public Layouter(Backend back, int indentation) {
224: this .back = back;
225: out = new Printer(back);
226: largeSize = 2 * back.lineWidth();
227: this .defaultInd = indentation;
228: }
229:
230: // CONVENIENCE CONSTRUCTORS ----------------------------------------
231:
232: /** = 80 : The line width for some of the convenience constructors.*/
233: public static final int DEFAULT_LINE_WIDTH = 80;
234:
235: /** = 2 : The default indentation for some of the convenience
236: constructors */
237: public static final int DEFAULT_INDENTATION = 2;
238:
239: /** Convenience constructor for a Layouter with a {@link WriterBackend}.
240: * The line width is taken to be {@link #DEFAULT_LINE_WIDTH}, and the
241: * default indentation {@link #DEFAULT_INDENTATION}.
242: *
243: * @param writer the {@link java.io.Writer} the Backend is going to use
244: */
245: public Layouter(java.io.Writer writer) {
246: this (writer, DEFAULT_LINE_WIDTH);
247: }
248:
249: /** Convenience constructor for a Layouter with a {@link WriterBackend}.
250: * The default indentation is taken from {@link #DEFAULT_INDENTATION}.
251: *
252: * @param writer the {@link java.io.Writer} the Backend is going to use
253: * @param lineWidth the maximum lineWidth the Backend is going to use
254: */
255: public Layouter(java.io.Writer writer, int lineWidth) {
256: this (writer, lineWidth, DEFAULT_INDENTATION);
257: }
258:
259: /** Convenience constructor for a Layouter with a {@link WriterBackend}.
260: *
261: * @param writer the {@link java.io.Writer} the Backend is going to use
262: * @param lineWidth the maximum lineWidth the Backend is going to use
263: * @param indentation the default indentation
264: */
265: public Layouter(java.io.Writer writer, int lineWidth,
266: int indentation) {
267: this (new WriterBackend(writer, lineWidth), indentation);
268: }
269:
270: // PRIMITIVE STREAM OPERATIONS ------------------------------------
271:
272: /** Output text material. The string <code>s</code> should not
273: * contain newline characters. If you have a string with newline
274: * characters, and want to retain its formatting, consider using
275: * the {@link #pre(String s)} method. The Layouter will not
276: * insert any line breaks in such a string.
277: *
278: * @param s the String to print.
279: * @return this
280: */
281: public Layouter print(String s) throws IOException {
282: if (delimStack.isEmpty()) {
283: out.print(s);
284: totalSize += back.measure(s);
285: totalOutput += back.measure(s);
286: } else {
287: enqueue(new StringToken(s));
288: totalSize += back.measure(s);
289:
290: while (totalSize - totalOutput > out.space()
291: && !delimStack.isEmpty()) {
292: popBottom().setInfiniteSize();
293: advanceLeft();
294: }
295: }
296: return this ;
297: }
298:
299: /** Begin a block. If <code>consistent</code> is set, breaks
300: * are either all broken or all not broken. The indentation
301: * level is increased by <code>indent</code>.
302: *
303: * @param consistent <code>true</code> for consistent block
304: * @param indent increment to indentation level
305: * @return this
306: */
307: public Layouter begin(boolean consistent, int indent) {
308: StreamToken t = new OpenBlockToken(consistent, indent);
309: enqueue(t);
310: push(t);
311: return this ;
312: }
313:
314: /** Ends the innermost block.
315: * @return this
316: **/
317: public Layouter end() throws IOException {
318: if (delimStack.isEmpty()) {
319: /* then stream is also empty, so output */
320: out.closeBlock();
321: } else {
322: enqueue(new CloseBlockToken());
323:
324: StreamToken topDelim = pop();
325: topDelim.setEnd();
326: if (topDelim instanceof BreakToken && !delimStack.isEmpty()) {
327: /* This must be the matching OpenBlockToken */
328: StreamToken topOpen = pop();
329: topOpen.setEnd();
330: }
331:
332: if (delimStack.isEmpty()) {
333: /* preserve invariant */
334: advanceLeft();
335: }
336: }
337: return this ;
338: }
339:
340: /**
341: * Print a break. This will print <code>width</code> spaces if the
342: * line is <em>not</em> broken at this point. If it <em>is</em>
343: * broken, indentation is added to the current indentation level,
344: * plus the value of <code>offset</code>.
345: *
346: * @param width space to insert if not broken
347: * @param offset offset relative to current indentation level
348: * @return this
349: */
350: public Layouter brk(int width, int offset) throws IOException {
351: if (!delimStack.isEmpty()) {
352: StreamToken s = top();
353: if (s instanceof BreakToken) {
354: pop();
355: s.setEnd();
356: }
357: }
358:
359: StreamToken t = new BreakToken(width, offset);
360: enqueue(t);
361: push(t);
362: totalSize += width;
363: return this ;
364: }
365:
366: /**
367: * Indent to a current indentation level if surrounding block is
368: * broken. If the surrounding block fits on one line, insert
369: * <code>width</code> spaces. Otherwise, indent to the current
370: * indentation level, plus <code>offset</code>, unless that
371: * position has already been exceeded on the current line. If
372: * that is the case, nothing is printed. No line break is
373: * possible at this point.
374: *
375: * @param width space to insert if not broken
376: * @param offset offset relative to current indentation level
377: * @return this
378: */
379: public Layouter ind(int width, int offset) throws IOException {
380: if (delimStack.isEmpty()) {
381: out.indent(width, offset);
382: totalSize += width;
383: totalOutput += width;
384: } else {
385: enqueue(new IndentationToken(width, offset));
386: totalSize += width;
387: }
388: return this ;
389: }
390:
391: /**
392: * This leads to a call of the {@link Backend#mark(Object)} method
393: * of the backend, when the material preceding the call to
394: * <code>mark</code> has been printed to the backend, including
395: * any inserted line breaks and indentation. The {@link Object}
396: * argument to <code>mark</code> is passed through unchanged to
397: * the backend and may be used by the application to pass
398: * information about the purpose of the mark.
399: *
400: * @param o an object to be passed through to the backend.
401: * @returns this
402: *
403: */
404: public Layouter mark(Object o) {
405: if (delimStack.isEmpty()) {
406: out.mark(o);
407: } else {
408: enqueue(new MarkToken(o));
409: }
410: return this ;
411: }
412:
413: /**
414: * Output any information currently kept in buffers. This is
415: * essentially passed on to the backend. Note that material in
416: * blocks begun but not ended cannot be forced to the output by
417: * this method. Finish all blocks and call <code>flush</code> or
418: * {@link #close()} then.
419: *
420: * @return this
421: */
422: public Layouter flush() throws IOException {
423: out.flush();
424: return this ;
425: }
426:
427: /**
428: * Close the Layouter. No more methods should be called after
429: * this. All blocks begun must have been ended by this point.
430: * Any pending material is written to the backend, before the
431: * {@link Backend#close()} method of the backend is called, which
432: * closes any open I/O streams, etc.
433: *
434: */
435: public void close() throws IOException {
436: if (!delimStack.isEmpty()) {
437: throw new UnbalancedBlocksException();
438: } else {
439: advanceLeft();
440: }
441: out.close();
442: }
443:
444: // CONVENIENCE STREAM OPERATIONS ---------------------------------
445:
446: /** Begin an inconsistent block. Add this Layouter's default
447: * indentation to the indentation level.
448: * @return this
449: */
450: public Layouter beginI() {
451: return begin(false, defaultInd);
452: }
453:
454: /** Begin a consistent block. Add this Layouter's default
455: * indentation to the indentation level.
456: * @return this
457: */
458: public Layouter beginC() {
459: return begin(true, defaultInd);
460: }
461:
462: /** Begin an inconsistent block. Add <code>indent</code>
463: * to the indentation level.
464: * @param indent the indentation for this block
465: * @return this
466: */
467: public Layouter beginI(int indent) {
468: return begin(false, indent);
469: }
470:
471: /** Begin a consistent block. Add <code>indent</code>
472: * to the indentation level.
473: * @param indent the indentation for this block
474: * @return this
475: */
476: public Layouter beginC(int indent) {
477: return begin(true, indent);
478: }
479:
480: /** Begin a block with default indentation. Add this Layouter's
481: * default indentation to the indentation level.
482: * @param consistent <code>true</code> for consistent block
483: * @return this */
484: public Layouter begin(boolean consistent) {
485: return begin(consistent, defaultInd);
486: }
487:
488: /** Print a break with zero offset.
489: * @param width space to insert if not broken
490: * @return this */
491: public Layouter brk(int width) throws IOException {
492: return brk(width, 0);
493: }
494:
495: /** Print a break with zero offset and width one.
496: * @return this */
497: public Layouter brk() throws IOException {
498: return brk(1);
499: }
500:
501: /** Print a break with zero offset and large width. As the large
502: * number of spaces will never fit into one line, this amounts to
503: * a forced line break.
504: * @return this */
505: public Layouter nl() throws IOException {
506: return brk(largeSize);
507: }
508:
509: /** Indent with zero offset and zero width. Just indents
510: * to the current indentation level if the block is broken, and
511: * prints nothing otherwise.
512: * @return this */
513: public Layouter ind() throws IOException {
514: return this .ind(0, 0);
515: }
516:
517: /** Layout prefromated text. This amounts to a (consistent) block
518: * with indentation 0, where each line of <code>s</code>
519: * (separated by \n) gets printed as a string and newlines become
520: * forced breaks.
521: * @param s the pre-formatted string
522: * @return this
523: */
524: public Layouter pre(String s) throws IOException {
525: StringTokenizer st = new StringTokenizer(s, "\n", true);
526: beginC(0);
527: while (st.hasMoreTokens()) {
528: String line = st.nextToken();
529: if ("\n".equals(line)) {
530: nl();
531: } else {
532: print(line);
533: }
534: }
535: end();
536:
537: return this ;
538: }
539:
540: // PRIVATE METHODS -----------------------------------------------
541:
542: /* Delimiter Stack handling */
543:
544: /** Push an OpenBlockToken or BreakToken onto the delimStack */
545: private void push(StreamToken t) {
546: delimStack.add(t);
547: }
548:
549: /** Pop the topmost Token from the delimStack */
550: private StreamToken pop() {
551: try {
552: return (StreamToken) (delimStack
553: .remove(delimStack.size() - 1));
554: } catch (IndexOutOfBoundsException e) {
555: throw new UnbalancedBlocksException();
556: }
557: }
558:
559: /** Remove and return the token from the <em>bottom</em> of the
560: * delimStack */
561: private StreamToken popBottom() {
562: try {
563: return (StreamToken) (delimStack.remove(0));
564: } catch (IndexOutOfBoundsException e) {
565: throw new UnbalancedBlocksException();
566: }
567: }
568:
569: /** Return the top of the delimStack, without popping it. */
570: private StreamToken top() {
571: try {
572: return (StreamToken) delimStack.get(delimStack.size() - 1);
573: } catch (IndexOutOfBoundsException e) {
574: throw new UnbalancedBlocksException();
575: }
576: }
577:
578: /* stream handling */
579:
580: /** Put a StreamToken into the stream (at the end). */
581: private void enqueue(StreamToken t) {
582: stream.add(t);
583: }
584:
585: /** Get the front token from the stream. */
586: private StreamToken dequeue() {
587: return (StreamToken) (stream.remove(0));
588: }
589:
590: /** Send tokens from <code>stream<code> to <code>out</code> as long
591: * as there are tokens left and their size is known. */
592: private void advanceLeft() throws IOException {
593: StreamToken t;
594: while (!stream.isEmpty()
595: && ((t = (StreamToken) stream.get(0))
596: .followingSizeKnown())) {
597: t.print();
598: stream.remove(0);
599: totalOutput += t.size();
600: }
601: }
602:
603: // STREAM TOKEN CLASSES -----------------------------------------
604:
605: /** A stream token.
606: */
607: private abstract class StreamToken {
608: /** Send this token to the Printer {@link #out}. */
609: abstract void print() throws IOException;
610:
611: /** Return the size of this token if the block is not broken. */
612: abstract int size();
613:
614: /** Return the `section' size. For an OpenBlockToken, this is the
615: * size of the whole block, if it is not broken. For a BreakToken,
616: * it is the size of the material up to the next corresponding
617: * BreakToken or CloseBlockToken. Otherwise it is the same as
618: * size(). This might only be known after several more tokens
619: * have been read. If the value is guaranteed to be larger than
620: * what fits on a line, some large value might be returned instead
621: * of the precise size.
622: */
623: int followingSize() {
624: return size();
625: }
626:
627: /** Returns whether the followingSize is already known. That
628: * is the case if either a corresponding next BreakToken or
629: * CloseBlockToken has been encountered, or if the material
630: * is known not to fit on a line.*/
631: boolean followingSizeKnown() {
632: return true;
633: }
634:
635: /** Indicate that the corresponding next BreakToken or
636: * CloseBlockToken has been encountered.
637: * After this, followingSizeKnown() will return the correct value.
638: */
639: void setEnd() {
640: throw new UnsupportedOperationException();
641: }
642:
643: /** Indicate that the followingSize is guaranteed to be larger than
644: * the line width, and that it can thus be set to some large value.
645: */
646: void setInfiniteSize() {
647: throw new UnsupportedOperationException();
648: }
649: }
650:
651: /** A token corresponding to a <code>print</code> call. */
652: private class StringToken extends StreamToken {
653: String s;
654:
655: StringToken(String s) {
656: this .s = s;
657: }
658:
659: void print() throws IOException {
660: out.print(s);
661: }
662:
663: int size() {
664: return back.measure(s);
665: }
666: }
667:
668: /** A token corresponding to an <code>ind</code> call. */
669: private class IndentationToken extends StreamToken {
670: protected int width;
671: protected int offset;
672:
673: IndentationToken(int width, int offset) {
674: this .width = width;
675: this .offset = offset;
676: }
677:
678: void print() throws IOException {
679: out.indent(width, offset);
680: }
681:
682: int size() {
683: return width;
684: }
685: }
686:
687: /** Superclass of tokens which calculate their followingSize. */
688: private abstract class SizeCalculatingToken extends StreamToken {
689: protected int begin = 0;
690: /** negative means that end has not been set yet.*/
691: protected int end = -1;
692:
693: SizeCalculatingToken() {
694: begin = totalSize;
695: }
696:
697: int followingSize() {
698: return end - begin;
699: }
700:
701: boolean followingSizeKnown() {
702: return end >= 0;
703: }
704:
705: void setEnd() {
706: this .end = totalSize;
707: }
708:
709: void setInfiniteSize() {
710: end = begin + largeSize;
711: }
712: }
713:
714: /** A token corresponding to a <code>brk</code> call. */
715: private class BreakToken extends SizeCalculatingToken {
716: protected int width;
717: protected int offset;
718:
719: BreakToken(int width, int offset) {
720: this .width = width;
721: this .offset = offset;
722: }
723:
724: int size() {
725: return width;
726: }
727:
728: void print() throws IOException {
729: out.printBreak(width, offset, followingSize());
730: }
731:
732: }
733:
734: /** A token corresponding to a <code>begin</code> call. */
735: private class OpenBlockToken extends SizeCalculatingToken {
736: protected boolean consistent;
737: protected int indent;
738:
739: OpenBlockToken(boolean consistent, int indent) {
740: this .consistent = consistent;
741: this .indent = indent;
742: }
743:
744: int size() {
745: return 0;
746: }
747:
748: void print() throws IOException {
749: out.openBlock(consistent, indent, followingSize());
750: }
751: }
752:
753: /** A token corresponding to an <code>end</code> call. */
754: private class CloseBlockToken extends StreamToken {
755:
756: CloseBlockToken() {
757: }
758:
759: void print() throws IOException {
760: out.closeBlock();
761: }
762:
763: int size() {
764: return 0;
765: }
766:
767: }
768:
769: /** A token corresponding to a <code>mark</code> call. */
770: private class MarkToken extends StreamToken {
771: protected Object o;
772:
773: MarkToken(Object o) {
774: this .o = o;
775: }
776:
777: int size() {
778: return 0;
779: }
780:
781: void print() {
782: out.mark(o);
783: }
784: }
785:
786: }
|