001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2011, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.bo.parser;
017
018 import java.util.Stack;
019
020 import org.qedeq.base.io.TextInput;
021
022 /**
023 * Remember TextInput positions.
024 *
025 * @author Michael Meyling
026 */
027 public class MementoTextInput {
028
029 /** For remembering input positions. */
030 private final Stack stack = new Stack();
031
032 /** Input source to parse. */
033 private final TextInput input;
034
035 /**
036 * Constructor.
037 *
038 * @param input Input source to parse.
039 */
040 public MementoTextInput(final TextInput input) {
041 this.input = input;
042 }
043
044 /**
045 * Remember current position.
046 */
047 public void markPosition() {
048 stack.push(new Integer(input.getPosition()));
049 }
050
051 /**
052 * Rewind to previous marked position. Also clears the mark.
053 *
054 * @return Current position before pop.
055 */
056 public long rewindPosition() {
057 final long oldPosition = getPosition();
058 input.setPosition(((Integer) stack.pop()).intValue());
059 return oldPosition;
060 }
061
062 /**
063 * Forget last remembered position.
064 */
065 public void clearMark() {
066 stack.pop();
067 }
068
069 /**
070 * Get byte position.
071 *
072 * @return Position.
073 */
074 public long getPosition() {
075 return input.getPosition();
076 }
077
078 /**
079 * Reads a single character and does not change the reading
080 * position.
081 *
082 * @return character read, if there are no more chars
083 * <code>-1</code> is returned
084 */
085 public int getChar() {
086 return input.getChar();
087 }
088
089 /**
090 * Reads a single character and increments the reading position
091 * by one.
092 *
093 * @return character read, if there are no more chars
094 * <code>-1</code> is returned
095 */
096 public int read() {
097 return input.read();
098 }
099
100 /**
101 * Are there still any characters to read?
102 *
103 * @return Anything left for reading further?
104 */
105 public final boolean isEmpty() {
106 return input.isEmpty();
107 }
108
109 /**
110 * Get rewind stack size.
111 *
112 * @return Rewind stack size.
113 */
114 public int getRewindStackSize() {
115 return stack.size();
116 }
117
118 /**
119 * Returns the current column number.
120 *
121 * @return Current column number (starting with line 1).
122 */
123 public int getColumn() {
124 return input.getColumn();
125 }
126
127 /**
128 * Returns the current line number.
129 *
130 * @return Current line number (starting with line 1).
131 */
132 public int getRow() {
133 return input.getRow();
134 }
135
136 /**
137 * Returns the current line.
138 *
139 * @return Current line.
140 */
141 public String getLine() {
142 return input.getLine();
143 }
144
145 /**
146 * Decrements the reading position by one and reads a single character.
147 * If no characters are left, <code>-1</code> is returned.
148 * Otherwise a cast to <code>char</code> gives the character read.
149 *
150 * @return Character read, if there are no more chars
151 * <code>-1</code> is returned.
152 */
153 public int readInverse() {
154 return input.readInverse();
155 }
156
157 }
|