2020-05-10 15:56:34 +02:00
|
|
|
|
|
|
|
import * as path from "path"
|
2020-05-23 22:48:24 +02:00
|
|
|
import * as fs from "fs"
|
2020-06-07 00:21:15 +02:00
|
|
|
import { serializeTag, serialize } from "./util";
|
2020-05-10 15:56:34 +02:00
|
|
|
|
|
|
|
export class TextFile {
|
|
|
|
|
2020-05-23 22:48:24 +02:00
|
|
|
private cachedText: string | null = null;
|
|
|
|
|
2020-05-10 15:56:34 +02:00
|
|
|
constructor(public origPath: string) {
|
|
|
|
|
|
|
|
}
|
|
|
|
|
2020-05-23 22:48:24 +02:00
|
|
|
public get fullPath() {
|
2020-05-10 15:56:34 +02:00
|
|
|
return path.resolve(this.origPath)
|
|
|
|
}
|
|
|
|
|
2020-06-07 00:21:15 +02:00
|
|
|
[serializeTag]() {
|
|
|
|
return this.origPath;
|
|
|
|
}
|
|
|
|
|
|
|
|
public getText(encoding: BufferEncoding = 'utf8'): string {
|
2020-05-23 22:48:24 +02:00
|
|
|
if (this.cachedText !== null) {
|
|
|
|
return this.cachedText;
|
|
|
|
}
|
2020-06-07 00:21:15 +02:00
|
|
|
const text = fs.readFileSync(this.fullPath, encoding);
|
2020-05-23 22:48:24 +02:00
|
|
|
this.cachedText = text;
|
|
|
|
return text
|
|
|
|
}
|
|
|
|
|
2020-05-10 15:56:34 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
export class TextPos {
|
|
|
|
|
|
|
|
constructor(
|
|
|
|
public offset: number,
|
|
|
|
public line: number,
|
|
|
|
public column: number
|
|
|
|
) {
|
|
|
|
|
|
|
|
}
|
|
|
|
|
2020-05-23 22:48:24 +02:00
|
|
|
public clone() {
|
2020-05-10 15:56:34 +02:00
|
|
|
return new TextPos(this.offset, this.line, this.column)
|
|
|
|
}
|
|
|
|
|
2020-06-07 00:21:15 +02:00
|
|
|
[serializeTag]() {
|
|
|
|
return {
|
|
|
|
offset: this.offset,
|
|
|
|
line: this.line,
|
|
|
|
column: this.column,
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
public advance(str: string) {
|
|
|
|
for (const ch of str) {
|
|
|
|
if (ch === '\n') {
|
|
|
|
this.line++;
|
|
|
|
this.column = 1;
|
|
|
|
} else {
|
|
|
|
this.column++;
|
|
|
|
}
|
|
|
|
this.offset++;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2020-05-10 15:56:34 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
export class TextSpan {
|
|
|
|
|
|
|
|
constructor(
|
|
|
|
public file: TextFile,
|
|
|
|
public start: TextPos,
|
|
|
|
public end: TextPos
|
|
|
|
) {
|
|
|
|
|
|
|
|
}
|
|
|
|
|
2020-05-23 22:48:24 +02:00
|
|
|
public clone() {
|
2020-05-10 15:56:34 +02:00
|
|
|
return new TextSpan(this.file, this.start.clone(), this.end.clone());
|
|
|
|
}
|
|
|
|
|
2020-06-07 00:21:15 +02:00
|
|
|
[serializeTag]() {
|
|
|
|
return {
|
|
|
|
file: serialize(this.file),
|
|
|
|
start: serialize(this.start),
|
|
|
|
end: serialize(this.end),
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2020-05-10 15:56:34 +02:00
|
|
|
}
|
|
|
|
|