001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 package javafe.util; 004 005 import java.io.IOException; 006 import javafe.genericfile.GenericFile; 007 008 /** 009 * This CorrelatedReader is built on top of another, given CorrelatedReader. 010 * All of the methods in this class simply call the corresponding methods 011 * on the underlying CorrelatedReader. 012 * 013 * @see javafe.util.CorrelatedReader 014 * @author Rustan Leino 015 */ 016 017 public class FilterCorrelatedReader extends CorrelatedReader 018 { 019 // Creation 020 021 protected /*@ non_null */ CorrelatedReader child; 022 023 /* The following invariant mentions "marked", which is not declared in 024 * this class. The justification for why it's still okay to declare 025 * this invariant here is that all of the methods that modify "this.marked" 026 * are overridden in the current class and, furthermore, the client is 027 * not supposed to use "child" (hence, not "child.marked" either) after 028 * passing it to the constructor. 029 */ 030 //@ invariant marked == child.marked; 031 032 /** Constructs a FilterCorrelatedReader with <code>child</code> as the 033 * underlying CorrelatedReader. After calling this constructor, the 034 * caller should no longer use <code>child</code> directly. 035 */ 036 037 protected FilterCorrelatedReader(/*@ non_null */ CorrelatedReader child) { 038 child.clearMark(); 039 this.child = child; 040 } 041 042 // Misc 043 044 /** Returns the file underlying this correlated reader. 045 */ 046 047 public GenericFile getFile() { 048 return child.getFile(); 049 } 050 051 052 // Getting Locations 053 054 /** 055 * Returns the location of the last character read. If no 056 * character has been read yet, returns a whole-file location for 057 * this file. 058 */ 059 060 public int getLocation() { 061 return child.getLocation(); 062 } 063 064 // [Un]marking 065 066 /** See documentation in superclass. 067 */ 068 069 public void mark() { 070 child.mark(); 071 marked = true; 072 } 073 074 /** See documentation in superclass. 075 */ 076 077 public void clearMark() { 078 child.clearMark(); 079 marked = false; 080 } 081 082 /** See documentation in superclass. 083 */ 084 085 public void reset() throws IOException { 086 child.reset(); 087 marked = false; 088 } 089 090 public CorrelatedReader createReaderFromMark(int discard) 091 throws IndexOutOfBoundsException { 092 return child.createReaderFromMark(discard); 093 } 094 095 // I/O 096 097 /** 098 * Closes us. No other I/O operations may be called on us after 099 * we have been closed. 100 */ 101 102 public void close() { 103 child.close(); 104 super.close(); 105 } 106 107 /** 108 * Reads the next character from this input stream. 109 * Does unicode conversion. <p> 110 * 111 * 112 * Requires we are open.<p> 113 * 114 * @return A unicode character, or -1.<p> 115 */ 116 public int read() throws IOException { 117 return child.read(); 118 } 119 }