fix(teacher): 改善只读工具分页与读取预算
This commit is contained in:
1 parent
17c7e5c495
commit
56cefe84e7
8 files changed
+297
-56
No files matched your search
@@ -0,0 +1,58 @@
|
||||
export function readInteger(value: unknown, fallback: number, maximum = Number.MAX_SAFE_INTEGER): number {
|
||||
const result = value ?? fallback;
|
||||
if (typeof result !== 'number' || !Number.isSafeInteger(result) || result < 1 || result > maximum)
|
||||
throw new Error('Invalid read range');
|
||||
return result;
|
||||
}
|
||||
|
||||
export function textChunks(text: string): string[] {
|
||||
return [text.replaceAll('\r\n', '\n')];
|
||||
}
|
||||
|
||||
// JSON contains contiguous original text; columns count Unicode code points, starting at 1.
|
||||
export async function readPage(
|
||||
source: string,
|
||||
chunks: AsyncIterable<string> | Iterable<string>,
|
||||
args: Record<string, unknown>,
|
||||
maxBytes: number,
|
||||
): Promise<{ content: string; truncated: boolean }> {
|
||||
const start = readInteger(args.start_line, 1);
|
||||
const column = readInteger(args.start_column, 1);
|
||||
const count = readInteger(args.line_count, 120, 400);
|
||||
const chars: string[] = [];
|
||||
let lineNumber = 1, position = 1, more = false;
|
||||
outer: for await (const chunk of chunks) {
|
||||
for (const char of chunk) {
|
||||
if (lineNumber === start && char === '\n' && position < column)
|
||||
throw new Error('Column is past the line');
|
||||
if (lineNumber > start || (lineNumber === start && position >= column)) {
|
||||
if (lineNumber >= start + count || chars.length >= maxBytes) { more = true; break outer; }
|
||||
chars.push(char);
|
||||
}
|
||||
if (char === '\n') { lineNumber++; position = 1; } else position++;
|
||||
}
|
||||
}
|
||||
if (lineNumber < start || (lineNumber === start && position < column))
|
||||
throw new Error('Read position is past the source');
|
||||
const render = (length: number) => {
|
||||
let nextLine = start, nextColumn = column;
|
||||
for (let i = 0; i < length; i++) {
|
||||
if (chars[i] === '\n') { nextLine++; nextColumn = 1; } else nextColumn++;
|
||||
}
|
||||
const next = more || length < chars.length ? { start_line: nextLine, start_column: nextColumn } : null;
|
||||
return { content: JSON.stringify({ source, start_line: start, start_column: column,
|
||||
text: chars.slice(0, length).join(''), next }), truncated: next !== null };
|
||||
};
|
||||
const complete = render(chars.length);
|
||||
if (Buffer.byteLength(complete.content) <= maxBytes) return complete;
|
||||
let low = 0, high = chars.length;
|
||||
while (low < high) {
|
||||
const middle = Math.ceil((low + high) / 2);
|
||||
if (Buffer.byteLength(render(middle).content) <= maxBytes) low = middle;
|
||||
else high = middle - 1;
|
||||
}
|
||||
const page = render(low);
|
||||
if ((chars.length && !low) || Buffer.byteLength(page.content) > maxBytes)
|
||||
throw new Error('Read budget too small for a page');
|
||||
return page;
|
||||
}
|
||||
Reference in new issue
Block a user