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 08:36:15 +02:00
|
|
|
import { serializeTag, serialize, deserializable } from "./util";
|
2020-05-10 15:56:34 +02:00
|
|
|
|
2020-06-07 08:36:15 +02:00
|
|
|
@deserializable()
|
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]() {
|
2020-06-07 08:36:15 +02:00
|
|
|
return [ this.origPath ];
|
2020-06-07 00:21:15 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
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
|
|
|
}
|
|
|
|
|
2020-06-07 08:36:15 +02:00
|
|
|
@deserializable()
|
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]() {
|
2020-06-07 08:36:15 +02:00
|
|
|
return [
|
|
|
|
this.offset,
|
|
|
|
this.line,
|
|
|
|
this.column,
|
|
|
|
]
|
2020-06-07 00:21:15 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
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
|
|
|
}
|
|
|
|
|
2020-06-07 08:36:15 +02:00
|
|
|
@deserializable()
|
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]() {
|
2020-06-07 08:36:15 +02:00
|
|
|
return [
|
|
|
|
this.file,
|
|
|
|
this.start,
|
|
|
|
this.end,
|
|
|
|
]
|
2020-06-07 00:21:15 +02:00
|
|
|
}
|
|
|
|
|
2020-05-10 15:56:34 +02:00
|
|
|
}
|
|
|
|
|