001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 package javafe.util; 004 005 import java.io.*; 006 007 import javafe.genericfile.GenericFile; 008 009 /** 010 * A reader (aka input stream) that provides an associated 011 * <I>location</I> with each character read. 012 * 013 * <p> See javafe.util.Location for the interpretation of these locations. 014 * 015 * <p> This class also takes care of unicode conversion. A unicode 016 * character sequence consists of a backslash that is preceded by an 017 * even number of backslashes, followed by one or more 'u's, followed 018 * by four hexadecimal digits. This class converts each unicode character 019 * sequence into a single character. 020 * 021 * <p> This class also provides the ability to mark a specific point 022 * in the input stream, and to reposition the stream at the marked 023 * position. We also provide a method to create a new 024 * <code>CorrelatedReader</code> for the text between the marked 025 * position and the current point in the stream. Marking is also 026 * allowed on the new <code>CorrelatedReader</code> object. For 027 * efficiency, we also provide the facility to remove the mark from 028 * the stream.<p> 029 * 030 * @see javafe.util.Location 031 * @author Cormac Flanagan 032 */ 033 034 public abstract class CorrelatedReader 035 /* may later want "extends Reader" */ 036 { 037 // Creation 038 039 /** Simple constructor. Pretty boring, really. */ 040 //@ ensures !marked; 041 042 protected CorrelatedReader() {} 043 044 // Misc 045 046 /** Returns the file underlying this correlated reader. */ 047 //@ ensures \result != null; 048 049 public abstract GenericFile getFile(); 050 051 // Getting Locations 052 053 /** 054 * Returns the location of the last character read. If no 055 * character has been read yet, returns a whole-file location for 056 * this file. 057 */ 058 //@ ensures \result != Location.NULL; 059 060 public abstract int getLocation(); 061 062 // [Un]marking 063 064 /** 065 * True iff a mark has been set. 066 */ 067 068 /*@ spec_public */ protected boolean marked = false; 069 070 /** 071 * Marks the position of the current character in this input 072 * stream. A subsequent call to the <code>reset</code> method 073 * repositions this stream at the last marked position. <p> 074 * 075 * This method differs from 076 * <code>java.io.InputStream.readlimit</code> in that it does not 077 * take a <code>readlimit</code> argument. <p> 078 * 079 * @see javafe.util.CorrelatedReader#reset() 080 * @see javafe.util.CorrelatedReader#clearMark() 081 * @see javafe.util.CorrelatedReader#createReaderFromMark 082 */ 083 //-@ modifies marked; 084 //@ ensures marked; 085 086 public abstract void mark(); 087 088 /** 089 * Removes the mark (if any) from the input stream. 090 * 091 * @see javafe.util.CorrelatedReader#mark() 092 */ 093 //@ modifies marked; 094 //@ ensures !marked; 095 096 public abstract void clearMark(); 097 098 /** 099 * Repositions this stream to the position at the time the 100 * <code>mark</code> method was last called on this input stream. <p> 101 * 102 * Requires that the input stream had been previously marked 103 * via the <code>mark()</code> method. <p> 104 * 105 * If mark() is called before read(), then the mark will be 106 * restored to its previous value (and not the preceeding 107 * character().<p> 108 * 109 * @exception IOException if this stream is not marked. 110 * @see javafe.util.CorrelatedReader#mark() 111 */ 112 //@ requires marked; 113 //-@ modifies marked; 114 //@ ensures !marked; 115 116 public abstract void reset() throws IOException; 117 118 /** 119 * Creates a <code>CorrelatedReader</code> object for the input 120 * text from the marked position, to the current position. <p> 121 * 122 * Calls to <code>getLocation()</code> for characters from the 123 * new <code>CorrelatedReader</code> yield the same locations as 124 * calls to <code>getLocation()</code> for the same characters on 125 * this <code>CorrelatedReader</code>. <p> 126 * 127 * The <code>discard</code> argument specifies the number of 128 * characters to discard from the end of the 129 * sub-<code>CorrelatedReader</code>. <p> 130 * 131 * Clears the mark as a side-effect. <p> 132 * 133 * Requires that the input stream had been previously marked via 134 * the <code>mark()</code> method and that we have not been 135 * closed. <p> 136 * 137 * @exception IndexOutOfBoundsException if <code>discard</code> is 138 * negative or exceeds the number of marked characters 139 * 140 * @see javafe.util.BufferedCorrelatedReader#mark() 141 */ 142 //@ requires 0 <= discard; 143 //@ requires marked; 144 //@ modifies marked; 145 //@ ensures \result != null; 146 //@ ensures !marked; 147 148 public abstract CorrelatedReader createReaderFromMark(int discard) 149 throws IndexOutOfBoundsException; 150 151 // I/O 152 153 /** 154 * Closes us. No other I/O operations may be called on us after 155 * we have been closed. 156 */ 157 158 public void close() {} 159 160 /** 161 * Reads the next character from this input stream. Does unicode 162 * conversion. <p> 163 * 164 * Requires we are open.<p> 165 * 166 * @return A unicode character, or -1.<p> 167 */ 168 public abstract int read() throws IOException; 169 }