Class SourceFile


  • public class SourceFile
    extends java.lang.Object
    Cached data for a source file. Contains a map of line numbers to byte offsets, for quick searching of source lines.
    See Also:
    SourceFinder
    • Field Detail

      • data

        private byte[] data
      • lineNumberMap

        private int[] lineNumberMap
      • numLines

        private int numLines
    • Constructor Detail

      • SourceFile

        public SourceFile​(SourceFileDataSource dataSource)
        Constructor.
        Parameters:
        dataSource - the SourceFileDataSource object which will provide the data of the source file
    • Method Detail

      • intValueOf

        private static int intValueOf​(byte b)
      • getFullFileName

        public java.lang.String getFullFileName()
        Get the full path name of the source file (with directory).
      • getFullURI

        public java.net.URI getFullURI()
        Get the full URI of the source file (with directory).
      • getInputStream

        public java.io.InputStream getInputStream()
                                           throws java.io.IOException
        Get an InputStream on data.
        Returns:
        an InputStream on the data in the source file, starting from given offset
        Throws:
        java.io.IOException
      • getInputStreamFromOffset

        public java.io.InputStream getInputStreamFromOffset​(int offset)
                                                     throws java.io.IOException
        Get an InputStream on data starting at given offset.
        Parameters:
        offset - the start offset
        Returns:
        an InputStream on the data in the source file, starting at the given offset
        Throws:
        java.io.IOException
      • addLineOffset

        public void addLineOffset​(int offset)
        Add a source line byte offset. This method should be called for each line in the source file, in order.
        Parameters:
        offset - the byte offset of the next source line
      • getLineOffset

        public int getLineOffset​(int line)
        Get the byte offset in the data for a source line. Note that lines are considered to be zero-index, so the first line in the file is numbered zero.
        Parameters:
        line - the line number
        Returns:
        the byte offset in the file's data for the line, or -1 if the line is not valid
      • loadFileData

        private void loadFileData()
                           throws java.io.IOException
        Throws:
        java.io.IOException
      • setData

        private void setData​(byte[] data)
        Set the source file data.
        Parameters:
        data - the data
      • getLastModified

        public long getLastModified()