Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

## escjava.parser
Class JmlCorrelatedReader

    java.lang.Object
      javafe.util.CorrelatedReader
          javafe.util.FilterCorrelatedReader
              escjava.parser.JmlCorrelatedReader

public class JmlCorrelatedReader
extends FilterCorrelatedReader

This `FilterCorrelatedReader` creates the illusion that the additional \@-signs, etc. allowed in the JML annotation syntax are really just whitespace.

Author:
  Rustan Leino
See Also:
  `FilterCorrelatedReader`

Field Summary
`private boolean` | `allowSpecialSuffix` Indicates whether or not a sequence of consecutive special characters at the end of the comment are to be treated as white space.
`static int` | `C_COMMENT`
`static int` | `COMMENTS_KINDS`
`static int` | `EOL_COMMENT`
`static int` | `JAVADOC_COMMENT`
`private int` | `lastUnreturnedChar` If there are unreturned characters, lastUnreturnedChar indicates the last of these characters.
`private int` | `lastUnreturnedCharAtMark`
`private int` | `prefixMode` The lines of the input consist of (0) a number of whitespace characters, (1) a number of special characters ('@' in ordinary comments and '*' inside Javadoc comments), and followed by (2) the "real meat".
`private int` | `prefixModeAtMark`
`private int` | `specialCharacter` Indicates the special character.
`private int` | `unreturnedChars` This variable is included so that @-signs at the end of a pragma-containing comment can be ignored.
`private int` | `unreturnedCharsAtMark`

Fields inherited from class javafe.util.FilterCorrelatedReader
`child`

Fields inherited from class javafe.util.CorrelatedReader
`marked`

Constructor Summary
`protected` | `JmlCorrelatedReader(CorrelatedReader child, int commentKind)` Constructs a `JmlCorrelatedReader` with `child` as the underlying `CorrelatedReader`.

Method Summary
`int` | `getLocation()` Returns the location of the last character read.
`void` | `mark()` See documentation in superclass.
`int` | `read()` Reads the next character from this input stream.
`void` | `reset()` See documentation in superclass.

Methods inherited from class javafe.util.FilterCorrelatedReader
`clearMark, close, createReaderFromMark, getFile`

Methods inherited from class java.lang.Object
`clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait`

Field Detail

### EOL_COMMENT

    public static final int EOL_COMMENT

See Also:
  Constant Field Values

### C_COMMENT

    public static final int C_COMMENT

See Also:
  Constant Field Values

### JAVADOC_COMMENT

    public static final int JAVADOC_COMMENT

See Also:
  Constant Field Values

### COMMENTS_KINDS

    public static final int COMMENTS_KINDS

See Also:
  Constant Field Values

### prefixMode

    private int prefixMode

  The lines of the input consist of (0) a number of whitespace characters, (1) a number of special characters ('@' in ordinary comments and '*' inside Javadoc comments), and followed by (2) the "real meat". The variable `prefixMode` indicates which of these three segments are currently being scanned.

### specialCharacter

    private final int specialCharacter

  Indicates the special character.

### unreturnedChars

    private int unreturnedChars

  This variable is included so that @-signs at the end of a pragma-containing comment can be ignored. In particular, it counts the number of characters read but not reported. These characters will be a number of @-signs followed by one more character (or -1, if at end-of-pragma). @-signs that immediately follow the first whitespace characters on a line are always "reported" (since these are actually reported as spaces anyway). In the steady state of this correlated reader, `unreturnedChars` is non-zero only when `lastUnreturnedChar` is not an @-sign.

  unreturnedChars is not used (actually, is 0) when scanning Javadoc comments.

### lastUnreturnedChar

    private int lastUnreturnedChar

  If there are unreturned characters, lastUnreturnedChar indicates the last of these characters.

### allowSpecialSuffix

    private final boolean allowSpecialSuffix

  Indicates whether or not a sequence of consecutive special characters at the end of the comment are to be treated as white space. This is only done for the special character '@'.

### prefixModeAtMark

    private int prefixModeAtMark

### unreturnedCharsAtMark

    private int unreturnedCharsAtMark

### lastUnreturnedCharAtMark

    private int lastUnreturnedCharAtMark

Constructor Detail

### JmlCorrelatedReader

    protected JmlCorrelatedReader(CorrelatedReader child,
                                  int commentKind)

  Constructs a `JmlCorrelatedReader` with `child` as the underlying `CorrelatedReader`. After calling this constructor, the caller should no longer use `child` directly.

  `commentKind` is `EOL_COMMENT` to indicate a slash-slash comment, `C_COMMENT` to indicate an ordinary slash-star comment, and `JAVADOC_COMMENT` to indicate that the portion to be read resides inside a (pair of tags in a) Javadoc comment.

Method Detail

### read

    public int read()
             throws java.io.IOException

  Reads the next character from this input stream. Performs Unicode conversion and JML filtering. Requires that the stream is open.

  Overrides:
    `read` in class `FilterCorrelatedReader`
  Returns:
    A Unicode character, or -1.
  Throws:
    `java.io.IOException`

### getLocation

    public int getLocation()

  Description copied from class: `FilterCorrelatedReader`
  Returns the location of the last character read. If no character has been read yet, returns a whole-file location for this file.

  Overrides:
    `getLocation` in class `FilterCorrelatedReader`

### mark

    public void mark()

  Description copied from class: `FilterCorrelatedReader`
  See documentation in superclass.

  Overrides:
    `mark` in class `FilterCorrelatedReader`

### reset

    public void reset()
               throws java.io.IOException

  Description copied from class: `FilterCorrelatedReader`
  See documentation in superclass.

  Overrides:
    `reset` in class `FilterCorrelatedReader`
  Throws:
    `java.io.IOException`

Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

The ESC/Java2 Project Homepage