| |
|
| java.lang.Object de.uka.ilkd.key.util.pp.StringBackend
initOutLength | protected int initOutLength(Code) | | |
lineWidth | protected int lineWidth(Code) | | |
StringBackend | public StringBackend(StringBuffer sb, int lineWidth)(Code) | | Create a new StringBackend. This will append all output to
the given StringBuffer sb .
|
StringBackend | public StringBackend(int lineWidth)(Code) | | Create a new StringBackend. This will accumulate output in
a fresh, private StringBuffer.
|
count | public int count()(Code) | | Returns the number of characters written through this backend.
|
getString | public String getString()(Code) | | Returns the accumulated output
|
lineWidth | public int lineWidth()(Code) | | Returns the available space per line
|
mark | public void mark(Object o)(Code) | | Gets called to record a mark() call in the input.
|
measure | public int measure(String s)(Code) | | Returns the space required to print the String s
|
|
|
|