diff options
author | paltherr <paltherr@epfl.ch> | 2003-06-24 08:57:30 +0000 |
---|---|---|
committer | paltherr <paltherr@epfl.ch> | 2003-06-24 08:57:30 +0000 |
commit | 9753961477f1f648656ec130675ed1b78f4f73b1 (patch) | |
tree | 3d0d93f692d5f7ca3a0eedfe1b0b74eab6dd027d /sources/ch/epfl/lamp/util/SourceFile.java | |
parent | 3102d7d40fcc65e6174e84d5424cd45d688c0257 (diff) | |
download | scala-9753961477f1f648656ec130675ed1b78f4f73b1.tar.gz scala-9753961477f1f648656ec130675ed1b78f4f73b1.tar.bz2 scala-9753961477f1f648656ec130675ed1b78f4f73b1.zip |
- Removed file from encoded positions
Diffstat (limited to 'sources/ch/epfl/lamp/util/SourceFile.java')
-rw-r--r-- | sources/ch/epfl/lamp/util/SourceFile.java | 52 |
1 files changed, 1 insertions, 51 deletions
diff --git a/sources/ch/epfl/lamp/util/SourceFile.java b/sources/ch/epfl/lamp/util/SourceFile.java index 44dbf82506..68a6739cab 100644 --- a/sources/ch/epfl/lamp/util/SourceFile.java +++ b/sources/ch/epfl/lamp/util/SourceFile.java @@ -30,29 +30,6 @@ public class SourceFile { public static final byte SU = 0x1A; //######################################################################## - // Public Functions - - /** Returns the source file with the given id. */ - public static SourceFile fromId(int id) { - if (id <= 0 || files.size() < id) return UNKNOWN; - return (SourceFile)files.get(id - 1); - } - - /** Releases all source file. */ - public static void releaseAll() { - files.clear(); - } - - //######################################################################## - // Private Variables - - /** The unknown source file */ - private static final SourceFile UNKNOWN = new SourceFile(); - - /** The list containing all source files */ - private static final ArrayList files = new ArrayList(); - - //######################################################################## // Private Fields /** The name of this source file */ @@ -61,9 +38,6 @@ public class SourceFile { /** The content of source this file */ private final byte[] bytes; - /** The id of this source file */ - private final int id; - /** The encoding of this source file or null if unspecified */ private String encoding; @@ -74,16 +48,6 @@ public class SourceFile { private int nextIndex = 0; //######################################################################## - // Private Constructors - - /** Initializes a new instance. */ - private SourceFile() { - this.name = "<<unknown source file>>"; - this.bytes = normalize(new byte[0]); - this.id = 0; - } - - //######################################################################## // Public Constructors /** Initializes a new instance. */ @@ -105,8 +69,6 @@ public class SourceFile { public SourceFile(String name, byte[] bytes) { this.name = name; this.bytes = normalize(bytes); - this.id = files.size() + 1; - files.add(this); } //######################################################################## @@ -122,11 +84,6 @@ public class SourceFile { return bytes; } - /** Returns the id of this source file. */ - public int id() { - return id; - } - /** Sets the encoding of the file. */ public void setEncoding(String encoding) { this.encoding = encoding; @@ -165,14 +122,7 @@ public class SourceFile { return new Position(this, line, column); } - /** - * Returns the integer encoding the position of the given line and - * column of this source file. - */ - public int getEncodedPosition(int line, int column) { - return Position.encode(this, line, column); - } - + /** Returns the name of this source file. */ public String toString() { return name; } |