Clover Coverage Report
Coverage timestamp: Sa Aug 2 2008 13:56:27 CEST
../../../../../img/srcFileCovDistChart8.png 47% of files have more coverage
14   148   12   1,17
0   45   0,86   12
12     1  
1    
 
  MementoTextInput       Line # 30 14 12 76,9% 0.7692308
 
  (92)
 
1    /* $Id: MementoTextInput.java,v 1.1 2008/07/26 07:58:30 m31 Exp $
2    *
3    * This file is part of the project "Hilbert II" - http://www.qedeq.org
4    *
5    * Copyright 2000-2008, Michael Meyling <mime@qedeq.org>.
6    *
7    * "Hilbert II" is free software; you can redistribute
8    * it and/or modify it under the terms of the GNU General Public
9    * License as published by the Free Software Foundation; either
10    * version 2 of the License, or (at your option) any later version.
11    *
12    * This program is distributed in the hope that it will be useful,
13    * but WITHOUT ANY WARRANTY; without even the implied warranty of
14    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15    * GNU General Public License for more details.
16    */
17   
18    package org.qedeq.kernel.bo.parser;
19   
20    import java.util.Stack;
21   
22    import org.qedeq.base.io.TextInput;
23   
24    /**
25    * Remember TextInput positions.
26    *
27    * @version $Revision: 1.1 $
28    * @author Michael Meyling
29    */
 
30    public class MementoTextInput {
31   
32    /** For remembering input positions. */
33    private final Stack stack = new Stack();
34   
35    /** Input source to parse. */
36    private final TextInput input;
37   
38    /**
39    * Constructor.
40    *
41    * @param input Input source to parse.
42    */
 
43  92 toggle public MementoTextInput(final TextInput input) {
44  92 this.input = input;
45    }
46   
47    /**
48    * Remember current position.
49    */
 
50  15914 toggle public void markPosition() {
51  15914 stack.push(new Integer(input.getPosition()));
52    }
53   
54    /**
55    * Rewind to previous marked position. Also clears the mark.
56    *
57    * @return Current position before pop.
58    */
 
59  9232 toggle public long rewindPosition() {
60  9232 final long oldPosition = getPosition();
61  9232 input.setPosition(((Integer) stack.pop()).intValue());
62  9232 return oldPosition;
63    }
64   
65    /**
66    * Forget last remembered position.
67    */
 
68  6682 toggle public void clearMark() {
69  6682 stack.pop();
70    }
71   
72    /**
73    * Get byte position.
74    *
75    * @return Position.
76    */
 
77  9232 toggle public long getPosition() {
78  9232 return input.getPosition();
79    }
80   
81    /**
82    * Reads a single character and does not change the reading
83    * position.
84    *
85    * @return character read, if there are no more chars
86    * <code>Character.MAX_VALUE</code> is returned
87    */
 
88  65216 toggle public int getChar() {
89  65216 return input.getChar();
90    }
91   
92    /**
93    * Reads a single character and increments the reading position
94    * by one.
95    *
96    * @return character read, if there are no more chars
97    * <code>Character.MAX_VALUE</code> is returned
98    */
 
99  15149 toggle public int readChar() {
100  15149 return input.read();
101    }
102   
103    /**
104    * Are there still any characters to read?
105    *
106    * @return Anything left for reading further?
107    */
 
108  22381 toggle public final boolean eof() {
109  22381 return input.isEmpty();
110    }
111   
112    /**
113    * Get rewind stack size.
114    *
115    * @return Rewind stack size.
116    */
 
117  89 toggle public int getRewindStackSize() {
118  89 return stack.size();
119    }
120   
121    /**
122    * Returns the current column number.
123    *
124    * @return Current column number (starting with line 1).
125    */
 
126  0 toggle public int getColumn() {
127  0 return input.getColumn();
128    }
129   
130    /**
131    * Returns the current line number.
132    *
133    * @return Current line number (starting with line 1).
134    */
 
135  0 toggle public int getRow() {
136  0 return input.getRow();
137    }
138   
139    /**
140    * Returns the current line.
141    *
142    * @return Current line.
143    */
 
144  0 toggle public String getLine() {
145  0 return input.getLine();
146    }
147   
148    }