71   private int recordsize;  field in OnDiskArray
123 …public OnDiskArray(File filename, int magicseed, int extraheadersize, int recordsize, int initials…  in OnDiskArray()  argument
126     this.recordsize = recordsize;  in OnDiskArray()
147     file.writeInt(this.recordsize);  in OnDiskArray()
182 …public OnDiskArray(File filename, int magicseed, int extraheadersize, int recordsize, boolean writ…  in OnDiskArray()  argument
185     this.recordsize = recordsize;  in OnDiskArray()
240     map = file.getChannel().map(mode, headersize, recordsize * numrecs);  in mapArray()
267       if (file.readInt() != this.recordsize) {  in validateHeader()
273       this.recordsize = file.readInt();  in validateHeader()
314     long pos = headersize + index * recordsize;  in indexToFileposition()
351       map.limit(recordsize * (index + 1));  in getRecordBuffer()
352       map.position(recordsize * index);  in getRecordBuffer()
384     return recordsize;  in getRecordsize()