From 5777ba48baa583b3395db5d6a3124a470c60a94f Mon Sep 17 00:00:00 2001 From: jzxia Date: Thu, 2 Jul 2026 22:01:01 +0800 Subject: [PATCH 01/14] feat: in local pretty-printer, show JJParser's error message to user, move cursor to position if the error message contains a position --- .../client/resources/wasm/tptp4X_wasm.wasm | Bin 147060 -> 147060 bytes tptplus/client/src/extension.ts | 87 ++++++++++++++++-- tptplus/client/src/localPrettyPrinter.ts | 65 +++++++++---- .../client/src/localPrettyPrinterProcess.ts | 86 +++++++++++++---- tptplus/native/tptp-pretty/src/tptp4X_api.c | 6 +- 5 files changed, 201 insertions(+), 43 deletions(-) diff --git a/tptplus/client/resources/wasm/tptp4X_wasm.wasm b/tptplus/client/resources/wasm/tptp4X_wasm.wasm index 4157f2c83b2c573ee4d2d1bef7cc27725444b1c5..1203f0b940aac047afc606c1b26f76d09a32400a 100755 GIT binary patch delta 24 gcmezJhvUm1jt!Ss85x@|v$kJmW!!$5m1&^`0GRd)p8x;= delta 24 gcmezJhvUm1jt!Ss85x={v$kJmW!!$5m1&^`0GQ|so&W#< diff --git a/tptplus/client/src/extension.ts b/tptplus/client/src/extension.ts index 9750727..54771ab 100644 --- a/tptplus/client/src/extension.ts +++ b/tptplus/client/src/extension.ts @@ -18,6 +18,63 @@ import { formatTptpLocally } from './localPrettyPrinter'; let client: LanguageClient; +/** + * Takes a JJParser error message and turns it into a VS Code cursor position. + * @param message The expected message shape is like + * "SyntaxError: Line 15 Char 6 Token "{" continuing with ..." + * @returns VS Code cursor position or undefined + */ +function parserErrorPosition(document: vscode.TextDocument, message: string): vscode.Position | undefined { + const match = message.match(/\bLine\s+(\d+)\s+Char\s+(\d+)(?:\s+Token\s+"([^"]*)")?/); + if (!match) { + return undefined; + } + + const reportedLine = Number.parseInt(match[1], 10); + const reportedCharacter = Number.parseInt(match[2], 10); + if (Number.isNaN(reportedLine) || Number.isNaN(reportedCharacter)) { + return undefined; + } + + const lineIndex = Math.max(0, Math.min(reportedLine - 1, document.lineCount - 1)); + const lineText = document.lineAt(lineIndex).text; + let characterIndex = Math.max(0, Math.min(reportedCharacter - 1, lineText.length)); + const token = match[3]; + + // If the error message reports a token, try to move cursor to the beginning of that token. + if (token) { + const tokenIndex = lineText.slice(0, characterIndex + 1).lastIndexOf(token); + if (tokenIndex >= 0) { + characterIndex = tokenIndex; + } + } + + return new vscode.Position(lineIndex, characterIndex); +} + +/** + * Takes a JJParser error message and, if it points to a specific position in source file, + * highlight the position. + * @param message The expected message shape is like + * "SyntaxError: Line 15 Char 6 Token "{" continuing with ..." + * @returns Whether the JJParser error message contains the description of a position + */ +async function revealParserErrorLocation(document: vscode.TextDocument, message: string): Promise { + const position = parserErrorPosition(document, message); + if (!position) { + return false; + } + + const range = new vscode.Range(position, position); + const editor = await vscode.window.showTextDocument(document, { + preview: false, + selection: range, + }); + editor.selection = new vscode.Selection(position, position); + editor.revealRange(range, vscode.TextEditorRevealType.InCenterIfOutsideViewport); + return true; +} + export function activate(context: ExtensionContext) { async function fetchList(url: string, inputType: string = 'radio') { @@ -339,16 +396,34 @@ export function activate(context: ExtensionContext) { // use WorkspaceEdit to edit any URI's document, even if it's invisible const edit = new vscode.WorkspaceEdit(); - const localOutput = - !sourceText.trim() ? "" : // a whitespace-only file should become empty - await formatTptpLocally(context, sourceText); - if (localOutput !== undefined) { - edit.replace(uri, fullTextRange, localOutput); + // a whitespace-only file should become empty + if (!sourceText.trim()) { + edit.replace(uri, fullTextRange, ""); + await vscode.workspace.applyEdit(edit); + return; + } + + // call the local pretty-printer + const localResult = await formatTptpLocally(context, sourceText); + if (localResult.kind === 'success') { + edit.replace(uri, fullTextRange, localResult.output); await vscode.workspace.applyEdit(edit); return; } + if (localResult.kind === 'parser-error') { + const foundErrorLocation = await revealParserErrorLocation(document, localResult.message); + if (foundErrorLocation) { + vscode.window.showErrorMessage(`Failed to format TPTP file: ${localResult.message}`); + return; + } else { + vscode.window.showErrorMessage(`\ + Failed to format TPTP file locally: ${localResult.message} + Trying the remote formatter on System B4 TPTP...`); + } + } - // fall back to remote pretty-printer if the local pretty-printer fails + // Fall back to remote pretty-printer if the local pretty-printer fails on an unknown error + // or an error that does not point to any specific location in `sourceText`. const form = createSystemB4TptpForm(sourceText, null); const response = await fetch('https://tptp.org/cgi-bin/SystemOnTPTPFormReply', { method: 'POST', diff --git a/tptplus/client/src/localPrettyPrinter.ts b/tptplus/client/src/localPrettyPrinter.ts index 818c9d6..86c65da 100644 --- a/tptplus/client/src/localPrettyPrinter.ts +++ b/tptplus/client/src/localPrettyPrinter.ts @@ -2,47 +2,80 @@ import { spawn } from 'child_process'; import * as path from 'path'; import * as vscode from 'vscode'; +const RUNNER_PATH = path.join('client', 'out', 'localPrettyPrinterProcess.js'); const LOCAL_PRETTY_PRINT_TIMEOUT_MS = 10000; +export type LocalPrettyPrintResult = + | { kind: 'success'; output: string } + | { kind: 'parser-error'; message: string } + | { kind: 'unknown-error' }; + +function readParserError(stderr: string): string | undefined { + for (const line of stderr.trim().split(/\r?\n/).reverse()) { + if (!line.trim()) { + continue; + } + + try { + const diagnostic = JSON.parse(line) as { kind?: unknown; message?: unknown }; + if (diagnostic.kind === 'jjparser' && typeof diagnostic.message === 'string') { + return diagnostic.message; + } + } catch { + // Ignore non-JSON stderr from the child process. + } + } + + return undefined; +} + export async function formatTptpLocally( context: vscode.ExtensionContext, input: string -): Promise { - const runnerPath = context.asAbsolutePath(path.join('client', 'out', 'localPrettyPrinterProcess.js')); - +): Promise { return new Promise(resolve => { let stdout = ''; + let stderr = ''; let settled = false; // prevent the promise from resolving twice - const child = spawn(process.execPath, [runnerPath], { + const child = spawn(process.execPath, [context.asAbsolutePath(RUNNER_PATH)], { env: { ...process.env, ELECTRON_RUN_AS_NODE: '1', }, - // parent can write to and read from child process; stderr is discarded - stdio: ['pipe', 'pipe', 'ignore'], + stdio: ['pipe', 'pipe', 'pipe'], // stdin, stdout, stderr }); - function finish(output: string | undefined): void { + function finish(result: LocalPrettyPrintResult): void { if (settled) return; settled = true; clearTimeout(timeout); - resolve(output); + resolve(result); } const timeout = setTimeout(() => { child.kill(); - finish(undefined); + finish({ + kind: 'parser-error', + message: `timeout after ${LOCAL_PRETTY_PRINT_TIMEOUT_MS} ms` + }); }, LOCAL_PRETTY_PRINT_TIMEOUT_MS); - child.on('error', () => finish(undefined)); - child.on('close', code => { - finish(code === 0 && stdout.length > 0 ? stdout : undefined); + child.on('error', () => finish({ kind: 'unknown-error' })); + child.on('close', exitCode => { + if (exitCode === 0) { + finish({ kind: 'success', output: stdout }); + } else { + const parserError = readParserError(stderr); + finish(parserError ? + { kind: 'parser-error', message: parserError } : + { kind: 'unknown-error' } + ); + } }); child.stdout.setEncoding('utf8'); - child.stdout.on('data', chunk => { - stdout += chunk; - }); - + child.stdout.on('data', chunk => { stdout += chunk; }); + child.stderr.setEncoding('utf8'); + child.stderr.on('data', chunk => { stderr += chunk; }); child.stdin.on('error', () => undefined); child.stdin.end(input, 'utf8'); }); diff --git a/tptplus/client/src/localPrettyPrinterProcess.ts b/tptplus/client/src/localPrettyPrinterProcess.ts index c3a9cc3..7f7ff6b 100644 --- a/tptplus/client/src/localPrettyPrinterProcess.ts +++ b/tptplus/client/src/localPrettyPrinterProcess.ts @@ -2,6 +2,9 @@ import * as fs from 'fs'; import * as path from 'path'; import createTPTP4X from '../resources/wasm/tptp4X_wasm.js'; +const WASM_DIR = path.join(__dirname, '..', 'resources', 'wasm'); +const WASM_BIN_PATH = path.join(WASM_DIR, 'tptp4X_wasm.wasm'); + export type TPTP4XModule = { lengthBytesUTF8(value: string): number; stringToUTF8(value: string, pointer: number, maxBytesToWrite: number): void; @@ -14,18 +17,62 @@ export type TPTP4XModule = { export type CreateTPTP4X = (options: { locateFile(file: string): string; - print(): void; - printErr(): void; + print(message?: string): void; + printErr(message?: string): void; quit(status: number, error: unknown): never; wasmBinary: ArrayBuffer | ArrayBufferView; }) => Promise; +const wasmDiagnostics: string[] = []; + function readStdin(): string { return fs.readFileSync(0, 'utf8'); } +function captureWasmDiagnostic(message?: string): void { + if (message && message.trim()) { + wasmDiagnostics.push(message); + } +} + +function parserDiagnosticMessage(): string | undefined { + const diagnosticStart = wasmDiagnostics.findIndex(message => + /^ERROR:\s/.test(message) || /^%\s*SZS status\s+\S+\s*:/.test(message) + ); + + if (diagnosticStart < 0) { + return undefined; + } + + const message = wasmDiagnostics.slice(diagnosticStart).join('\n'); + const errorMatch = message.match(/^ERROR:\s*(.*)$/s); + if (errorMatch) { + return errorMatch[1].trim(); + } + + const szsMatch = message.match(/^%\s*SZS status\s+(\S+)\s*:\s*(.*)$/s); + if (szsMatch) { + return `${szsMatch[1]}: ${szsMatch[2].trim()}`; + } + + return undefined; +} + +function writeParserDiagnostic(): void { + const message = parserDiagnosticMessage(); + + if (!message) { + return; + } + + process.stderr.write(`${JSON.stringify({ + kind: 'jjparser', + message, + })}\n`); +} + /** - * Copies a JavaScript string into WASM memory + * Copies a JavaScript string into WASM memory. * @param value - the string to be copied * @returns pointer to the copy in WASM memory */ @@ -41,31 +88,31 @@ function writeString(module: TPTP4XModule, value: string): number { return pointer; } +/** + * Returns a non-zero exit code (default = 1) by parsing an error of unknown type. + */ function statusFromError(error: unknown): number { - if ( - typeof error === 'object' && - error !== null && - 'status' in error && - typeof (error as { status?: unknown }).status === 'number' + if (error !== null && typeof error === 'object' && + 'status' in error && typeof error.status === 'number' ) { - return (error as { status: number }).status || 1; + return error.status || 1; } return 1; } async function main(): Promise { - const wasmDirectory = path.join(__dirname, '..', 'resources', 'wasm'); + let wasmExited = false; const module = await createTPTP4X({ - locateFile: (file: string) => path.join(wasmDirectory, file), - // print and printErr are silenced because stdout is reserved for the formatted TPTP output - print: () => undefined, - printErr: () => undefined, + locateFile: (file: string) => path.join(WASM_DIR, file), + print: captureWasmDiagnostic, + printErr: captureWasmDiagnostic, quit: (status: number, error: unknown): never => { + wasmExited = true; const throwable = error instanceof Error ? error : new Error(`WASM exited with status ${status}`); (throwable as Error & { status?: number }).status = status; throw throwable; }, - wasmBinary: fs.readFileSync(path.join(wasmDirectory, 'tptp4X_wasm.wasm')), + wasmBinary: fs.readFileSync(WASM_BIN_PATH), }); let inputPointer = 0; @@ -76,20 +123,23 @@ async function main(): Promise { outputPointer = module._tptp4x_pretty_print_tptp(inputPointer); if (!outputPointer) { - process.exit(1); + writeParserDiagnostic(); + process.exitCode = 1; + return; } process.stdout.write(module.UTF8ToString(outputPointer)); } finally { - if (outputPointer) { + if (outputPointer && !wasmExited) { module._tptp4x_free_string(outputPointer); } - if (inputPointer) { + if (inputPointer && !wasmExited) { module._free(inputPointer); } } } main().catch((error: unknown) => { + writeParserDiagnostic(); process.exit(statusFromError(error)); }); diff --git a/tptplus/native/tptp-pretty/src/tptp4X_api.c b/tptplus/native/tptp-pretty/src/tptp4X_api.c index b679573..267c073 100644 --- a/tptplus/native/tptp-pretty/src/tptp4X_api.c +++ b/tptplus/native/tptp-pretty/src/tptp4X_api.c @@ -100,9 +100,9 @@ char * tptp4x_pretty_print_tptp(const char * Input) { OldSZSStatusReporting = GetSZSStatusReporting(); SetNeedForNonLogicTokens(1); - SetAllowFreeVariables(0); + SetAllowFreeVariables(0); // no getter for AllowFreeVariables (default value is 0) SetWarnings(0); - SetSZSStatusReporting(0); + SetSZSStatusReporting(1); State->OutputStream = open_memstream(&(State->OutputBuffer), &(State->OutputLength)); if (State->OutputStream == NULL) { @@ -139,7 +139,7 @@ char * tptp4x_pretty_print_tptp(const char * Input) { finish: SetNeedForNonLogicTokens(OldNeedNonLogicTokens); - SetAllowFreeVariables(0); + SetAllowFreeVariables(0); // no getter for AllowFreeVariables (default value is 0) SetWarnings(OldWarnings); SetSZSStatusReporting(OldSZSStatusReporting); CleanupPrettyState((TPTP4XPrettyState *)State); From eebde91cb5d7c2df8111108322eeeeda565c8199 Mon Sep 17 00:00:00 2001 From: jzxia Date: Thu, 2 Jul 2026 22:16:48 +0800 Subject: [PATCH 02/14] remove button `TPTP: Format Document` because: - It takes up too much space in editor that could be used to display open tabs. - The command `TPTP: Format Document` will eventually be removed in favor of `TPTP: Format TPTP File` which calls JJParser locally. But at present, the former command should be kept as it supports range formatting (albeit with known bugs) while the latter doesn't. --- tptplus/package.json | 7 ------- 1 file changed, 7 deletions(-) diff --git a/tptplus/package.json b/tptplus/package.json index e1d39a9..9032ba8 100644 --- a/tptplus/package.json +++ b/tptplus/package.json @@ -84,13 +84,6 @@ } ], "menus": { - "editor/title": [ - { - "command": "tptp.formatDocument", - "when": "editorLangId == tptp", - "group": "navigation" - } - ], "editor/context": [ { "command": "tptp.prepareProblem", From 88240089bf94521bb5b64f61cdebd128d467ebb4 Mon Sep 17 00:00:00 2001 From: jzxia Date: Fri, 3 Jul 2026 13:04:56 +0800 Subject: [PATCH 03/14] feat: use JSDOM to extract from HTML response of SystemB4TPTP; error handling for remote pretty-printer --- tptplus/client/src/extension.ts | 84 +++++++++++++++++++----- tptplus/client/src/localPrettyPrinter.ts | 6 +- 2 files changed, 73 insertions(+), 17 deletions(-) diff --git a/tptplus/client/src/extension.ts b/tptplus/client/src/extension.ts index 54771ab..e662dd6 100644 --- a/tptplus/client/src/extension.ts +++ b/tptplus/client/src/extension.ts @@ -18,6 +18,47 @@ import { formatTptpLocally } from './localPrettyPrinter'; let client: LanguageClient; +/** + * Extract the text between `
` and `
` from the HTML response of System B4 TPTP. + */ +function extractSystemB4TptpOutput(html: string): string | undefined { + const dom = new JSDOM(html); + const preText = dom.window.document.querySelector('pre')?.textContent ?? undefined; + if (preText === undefined) { + return undefined; + } + + const startMarker = '% START OF SYSTEM OUTPUT'; + const endMarker = '% END OF SYSTEM OUTPUT'; + const lines = preText.split('\n'); + const startLine = lines.findIndex(line => line.trim() === startMarker); + let endLine = -1; // TODO: use `findLastIndex`? + for (let i = lines.length - 1; i >= Math.max(0, startLine); i -= 1) { + if (lines[i].trim() === endMarker) { + endLine = i; + break; + } + } + + if (startLine === -1 || endLine === -1 || startLine >= endLine) { + return undefined; + } + + return lines.slice(startLine + 1, endLine).join('\n'); +} + +function lastNonemptyLine(text: string): string | undefined { + const lines = text.split('\n'); + for (let i = lines.length - 1; i >= 0; i -= 1) { + const line = lines[i].trim(); + if (line) { + return line; + } + } + + return undefined; +} + /** * Takes a JJParser error message and turns it into a VS Code cursor position. * @param message The expected message shape is like @@ -276,7 +317,7 @@ export function activate(context: ExtensionContext) { body: form }); const text = await response.text(); - const match = text.match(/]*>([\s\S]*?)<\/pre>/i); + const formattedOutput = extractSystemB4TptpOutput(text); const editor = vscode.window.activeTextEditor; @@ -290,12 +331,18 @@ export function activate(context: ExtensionContext) { let output = document.getText(fullTextRange); - if (match) { - output = match[1].split("\n").slice(2, match[1].split("\n").length - 4).join("\n") + if (formattedOutput !== undefined) { + const lastLine = lastNonemptyLine(formattedOutput); + if (lastLine?.startsWith('ERROR: ')) { + await revealParserErrorLocation(document, lastLine); + return; + } + + output = formattedOutput } editor.edit(editBuilder => { - editBuilder.replace(fullTextRange, output.replace(/>/g, ">")); + editBuilder.replace(fullTextRange, output); }); } } @@ -375,7 +422,7 @@ export function activate(context: ExtensionContext) { context.subscriptions.push(prepareProblem); - //@ FORMAT A PROBLEM THROUGH SYSTEMB4TPTP + //@ FORMAT A PROBLEM BY RUNNING JJPARSER LOCALLY, USING REMOTE SYSTEMB4TPTP AS FALLBACK const formatProblem = vscode.commands.registerCommand('tptp.formatProblem', async (uri: vscode.Uri) => { if (!uri) { const activeEditor = vscode.window.activeTextEditor; @@ -403,7 +450,7 @@ export function activate(context: ExtensionContext) { return; } - // call the local pretty-printer + // call the local pretty-printer (JJParser) const localResult = await formatTptpLocally(context, sourceText); if (localResult.kind === 'success') { edit.replace(uri, fullTextRange, localResult.output); @@ -416,9 +463,9 @@ export function activate(context: ExtensionContext) { vscode.window.showErrorMessage(`Failed to format TPTP file: ${localResult.message}`); return; } else { - vscode.window.showErrorMessage(`\ + vscode.window.showWarningMessage(`\ Failed to format TPTP file locally: ${localResult.message} - Trying the remote formatter on System B4 TPTP...`); + Trying the remote formatter provided by SystemB4TPTP...`); } } @@ -430,16 +477,21 @@ export function activate(context: ExtensionContext) { body: form }); const text = await response.text(); - const match = text.match(/]*>([\s\S]*?)<\/pre>/i); - - let output = sourceText; + const formattedOutput = extractSystemB4TptpOutput(text); - if (match) { - output = match[1].split("\n").slice(2, match[1].split("\n").length - 4).join("\n") + if (formattedOutput !== undefined) { + const lastLine = lastNonemptyLine(formattedOutput); + if (lastLine?.startsWith('ERROR: ')) { + await revealParserErrorLocation(document, lastLine); + vscode.window.showErrorMessage(`\ + Failed to format TPTP file: \ + remote formatter provided by SystemB4TPTP exited with ${lastLine}`); + } else { + edit.replace(uri, fullTextRange, formattedOutput); + await vscode.workspace.applyEdit(edit); + vscode.window.showInformationMessage("Format TPTP file successful."); + } } - - edit.replace(uri, fullTextRange, output.replace(/>/g, ">")); - await vscode.workspace.applyEdit(edit); }) diff --git a/tptplus/client/src/localPrettyPrinter.ts b/tptplus/client/src/localPrettyPrinter.ts index 86c65da..a56f5b8 100644 --- a/tptplus/client/src/localPrettyPrinter.ts +++ b/tptplus/client/src/localPrettyPrinter.ts @@ -3,7 +3,7 @@ import * as path from 'path'; import * as vscode from 'vscode'; const RUNNER_PATH = path.join('client', 'out', 'localPrettyPrinterProcess.js'); -const LOCAL_PRETTY_PRINT_TIMEOUT_MS = 10000; +const LOCAL_PRETTY_PRINT_TIMEOUT_MS = 10000; // TODO: make this configurable export type LocalPrettyPrintResult = | { kind: 'success'; output: string } @@ -33,6 +33,10 @@ export async function formatTptpLocally( context: vscode.ExtensionContext, input: string ): Promise { + + // // debugging: uncomment this to simulate a failure of the local JJParser + // return { kind: 'parser-error', message: '(This is an error message for debugging that does not point to any specific location in source file.)' }; + return new Promise(resolve => { let stdout = ''; let stderr = ''; From 8e31c7c14e7375b571b5fe2c5536395148fac12d Mon Sep 17 00:00:00 2001 From: jzxia Date: Fri, 3 Jul 2026 13:21:29 +0800 Subject: [PATCH 04/14] chore: publish v0.1.10: Added error handling for "Format TPTP File": display error message and jump to position of syntax error. --- README.md | 4 ++++ tptplus/CHANGELOG.md | 3 ++- tptplus/README.md | 4 ++++ 3 files changed, 10 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 0019cfe..b0641f4 100644 --- a/README.md +++ b/README.md @@ -161,6 +161,10 @@ Fixed issue where some greater-than-signs are not handled correctly by command " Added local pretty printer so that "Format TPTP File" works without Internet connection. The original remote pretty printer is kept as a fallback. +### 0.1.10 + +Added error handling for "Format TPTP File": display error message and jump to position of syntax error. + --- ## For TPTP Language diff --git a/tptplus/CHANGELOG.md b/tptplus/CHANGELOG.md index b683c06..0438c7e 100644 --- a/tptplus/CHANGELOG.md +++ b/tptplus/CHANGELOG.md @@ -21,4 +21,5 @@ - v0.1.5 Added dynamic loading of ATP systems from tptp.org by using fetch. - v0.1.7 Automated linting, and standardized releases with GitHub actions. - v0.1.8 Fixed issue where some greater-than-signs are not handled correctly by command "Format TPTP File". -- v0.1.9 Added local pretty printer so that "Format TPTP File" works without Internet connection. The original remote pretty printer is kept as a fallback. \ No newline at end of file +- v0.1.9 Added local pretty printer so that "Format TPTP File" works without Internet connection. The original remote pretty printer is kept as a fallback. +- v0.1.10 Added error handling for "Format TPTP File": display error message and jump to position of syntax error. \ No newline at end of file diff --git a/tptplus/README.md b/tptplus/README.md index 248d3c4..033fef0 100644 --- a/tptplus/README.md +++ b/tptplus/README.md @@ -160,6 +160,10 @@ Fixed issue where some greater-than-signs are not handled correctly by command " Added local pretty printer so that "Format TPTP File" works without Internet connection. The original remote pretty printer is kept as a fallback. +### 0.1.10 + +Added error handling for "Format TPTP File": display error message and jump to position of syntax error. + --- ## For TPTP Language From 01b1de99b3d47aed911f72515308cf7f37a65083 Mon Sep 17 00:00:00 2001 From: jzxia Date: Fri, 3 Jul 2026 13:27:08 +0800 Subject: [PATCH 05/14] chore: increase version number to v0.1.10 --- tptplus/package.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tptplus/package.json b/tptplus/package.json index 9032ba8..c4ffe45 100644 --- a/tptplus/package.json +++ b/tptplus/package.json @@ -3,7 +3,7 @@ "displayName": "TPTP", "publisher": "TPTPWorld", "description": "Syntax highlighting, error detection, pretty-printing, and proving & processing theorems functions for TPTP language", - "version": "0.1.9", + "version": "0.1.10", "icon": "images/TPTPWorld.png", "repository": { "type": "git", From cb6be81c6ac61e89832a202824f7fe3e8af2288c Mon Sep 17 00:00:00 2001 From: jzxia Date: Fri, 3 Jul 2026 15:22:21 +0800 Subject: [PATCH 06/14] revert unintended changes to `prepareProblem` --- tptplus/client/src/extension.ts | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/tptplus/client/src/extension.ts b/tptplus/client/src/extension.ts index e662dd6..15353f7 100644 --- a/tptplus/client/src/extension.ts +++ b/tptplus/client/src/extension.ts @@ -317,7 +317,7 @@ export function activate(context: ExtensionContext) { body: form }); const text = await response.text(); - const formattedOutput = extractSystemB4TptpOutput(text); + const match = text.match(/]*>([\s\S]*?)<\/pre>/i); const editor = vscode.window.activeTextEditor; @@ -331,18 +331,12 @@ export function activate(context: ExtensionContext) { let output = document.getText(fullTextRange); - if (formattedOutput !== undefined) { - const lastLine = lastNonemptyLine(formattedOutput); - if (lastLine?.startsWith('ERROR: ')) { - await revealParserErrorLocation(document, lastLine); - return; - } - - output = formattedOutput + if (match) { + output = match[1].split("\n").slice(2, match[1].split("\n").length - 4).join("\n") } editor.edit(editBuilder => { - editBuilder.replace(fullTextRange, output); + editBuilder.replace(fullTextRange, output.replace(/>/g, ">")); }); } } From 99a6445db0d57a1ef522f2c2dd7fd01639baba41 Mon Sep 17 00:00:00 2001 From: jzxia Date: Wed, 8 Jul 2026 16:59:15 +0800 Subject: [PATCH 07/14] feat: in `parserErrorPosition`, handle the case `Line .. Char .. Character "."` emitted by JJParser's `CharacterError` --- tptplus/client/src/extension.ts | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/tptplus/client/src/extension.ts b/tptplus/client/src/extension.ts index 15353f7..01f7fd1 100644 --- a/tptplus/client/src/extension.ts +++ b/tptplus/client/src/extension.ts @@ -62,11 +62,12 @@ function lastNonemptyLine(text: string): string | undefined { /** * Takes a JJParser error message and turns it into a VS Code cursor position. * @param message The expected message shape is like - * "SyntaxError: Line 15 Char 6 Token "{" continuing with ..." + * 'SyntaxError: Line 15 Char 6 Token "{" continuing with ...' or + * 'SyntaxError: Line 11 Char 42 Character "[" continuing with ...' * @returns VS Code cursor position or undefined */ function parserErrorPosition(document: vscode.TextDocument, message: string): vscode.Position | undefined { - const match = message.match(/\bLine\s+(\d+)\s+Char\s+(\d+)(?:\s+Token\s+"([^"]*)")?/); + const match = message.match(/\bLine\s+(\d+)\s+Char\s+(\d+)(?:\s+(?:Token|Character)\s+"([\s\S]*?)"\s+continuing\b)?/); if (!match) { return undefined; } @@ -80,13 +81,13 @@ function parserErrorPosition(document: vscode.TextDocument, message: string): vs const lineIndex = Math.max(0, Math.min(reportedLine - 1, document.lineCount - 1)); const lineText = document.lineAt(lineIndex).text; let characterIndex = Math.max(0, Math.min(reportedCharacter - 1, lineText.length)); - const token = match[3]; + const reportedText = match[3]; - // If the error message reports a token, try to move cursor to the beginning of that token. - if (token) { - const tokenIndex = lineText.slice(0, characterIndex + 1).lastIndexOf(token); - if (tokenIndex >= 0) { - characterIndex = tokenIndex; + // If the error message reports a token or character, try to move cursor to its beginning. + if (reportedText) { + const reportedTextIndex = lineText.slice(0, characterIndex + 1).lastIndexOf(reportedText); + if (reportedTextIndex >= 0) { + characterIndex = reportedTextIndex; } } From 07c80d12799cd13a6416482b98119fc7247a9a47 Mon Sep 17 00:00:00 2001 From: jzxia Date: Thu, 9 Jul 2026 15:02:18 +0800 Subject: [PATCH 08/14] feat: show diagnostics for JJParser errors and clear stale diagnostics on edits or new pretty-printer runs. --- tptplus/client/src/extension.ts | 102 +++++++++++++++++++++++++------- 1 file changed, 80 insertions(+), 22 deletions(-) diff --git a/tptplus/client/src/extension.ts b/tptplus/client/src/extension.ts index 01f7fd1..f4976ee 100644 --- a/tptplus/client/src/extension.ts +++ b/tptplus/client/src/extension.ts @@ -18,6 +18,13 @@ import { formatTptpLocally } from './localPrettyPrinter'; let client: LanguageClient; +interface JJParserErrorLocation { + position: vscode.Position; + range: vscode.Range; + message: string; + reportedText?: string; +} + /** * Extract the text between `
` and `
` from the HTML response of System B4 TPTP. */ @@ -60,13 +67,15 @@ function lastNonemptyLine(text: string): string | undefined { } /** - * Takes a JJParser error message and turns it into a VS Code cursor position. + * Takes a JJParser error message and turns it into a VS Code location. * @param message The expected message shape is like * 'SyntaxError: Line 15 Char 6 Token "{" continuing with ...' or * 'SyntaxError: Line 11 Char 42 Character "[" continuing with ...' - * @returns VS Code cursor position or undefined + * @returns VS Code location or undefined */ -function parserErrorPosition(document: vscode.TextDocument, message: string): vscode.Position | undefined { +function getJJParserErrorLocation(document: vscode.TextDocument, message: string): + JJParserErrorLocation | undefined +{ const match = message.match(/\bLine\s+(\d+)\s+Char\s+(\d+)(?:\s+(?:Token|Character)\s+"([\s\S]*?)"\s+continuing\b)?/); if (!match) { return undefined; @@ -91,20 +100,56 @@ function parserErrorPosition(document: vscode.TextDocument, message: string): vs } } - return new vscode.Position(lineIndex, characterIndex); + const startPosition = new vscode.Position(lineIndex, characterIndex); + const endCharacterIndex = reportedText + ? Math.min(lineText.length, characterIndex + reportedText.length) + : characterIndex; + const endPosition = new vscode.Position(lineIndex, endCharacterIndex); + + return { + position: startPosition, + range: new vscode.Range(startPosition, endPosition), + message: message, + reportedText: reportedText + }; } /** - * Takes a JJParser error message and, if it points to a specific position in source file, + * Adds a warning diagnostic for a JJParser-reported token or character. + * The squiggle and diagnostic message are cleared on document edit or before + * each new pretty-printer run. + */ +function setJJParserErrorDiagnostic( + diagnostics: vscode.DiagnosticCollection, + document: vscode.TextDocument, + errorLocation: JJParserErrorLocation | undefined +) { + if (!errorLocation?.reportedText) { + return; + } + + const diagnostic = new vscode.Diagnostic( + errorLocation.range, + errorLocation.message, + vscode.DiagnosticSeverity.Warning + ); + diagnostic.source = 'TPTP pretty-printer (JJParser)'; + diagnostics.set(document.uri, [diagnostic]); +} + +/** + * Takes a JJParser error location and, if it points to a specific position in source file, * highlight the position. - * @param message The expected message shape is like - * "SyntaxError: Line 15 Char 6 Token "{" continuing with ..." - * @returns Whether the JJParser error message contains the description of a position + * @param errorLocation The location parsed from a JJParser error message. */ -async function revealParserErrorLocation(document: vscode.TextDocument, message: string): Promise { - const position = parserErrorPosition(document, message); +async function revealJJParserErrorLocation( + document: vscode.TextDocument, + errorLocation: JJParserErrorLocation | undefined +): Promise +{ + const position = errorLocation?.position; if (!position) { - return false; + return; } const range = new vscode.Range(position, position); @@ -114,10 +159,16 @@ async function revealParserErrorLocation(document: vscode.TextDocument, message: }); editor.selection = new vscode.Selection(position, position); editor.revealRange(range, vscode.TextEditorRevealType.InCenterIfOutsideViewport); - return true; } export function activate(context: ExtensionContext) { + const prettyPrinterDiagnostics = vscode.languages.createDiagnosticCollection('tptpPrettyPrinter'); + context.subscriptions.push(prettyPrinterDiagnostics); + context.subscriptions.push( + vscode.workspace.onDidChangeTextDocument(event => { + prettyPrinterDiagnostics.delete(event.document.uri); + }) + ); async function fetchList(url: string, inputType: string = 'radio') { const response = await fetch(url, { @@ -413,7 +464,7 @@ export function activate(context: ExtensionContext) { } }) - }) + }); context.subscriptions.push(prepareProblem); @@ -428,6 +479,9 @@ export function activate(context: ExtensionContext) { uri = activeEditor.document.uri; } + // Clear stale parser diagnostics before each new pretty-printer run. + prettyPrinterDiagnostics.delete(uri); + const document = await vscode.workspace.openTextDocument(uri); const sourceText = document.getText(); const fullTextRange = new vscode.Range( @@ -453,8 +507,10 @@ export function activate(context: ExtensionContext) { return; } if (localResult.kind === 'parser-error') { - const foundErrorLocation = await revealParserErrorLocation(document, localResult.message); - if (foundErrorLocation) { + const errorLocation = getJJParserErrorLocation(document, localResult.message); + if (errorLocation !== undefined) { + setJJParserErrorDiagnostic(prettyPrinterDiagnostics, document, errorLocation); + await revealJJParserErrorLocation(document, errorLocation); vscode.window.showErrorMessage(`Failed to format TPTP file: ${localResult.message}`); return; } else { @@ -477,7 +533,9 @@ export function activate(context: ExtensionContext) { if (formattedOutput !== undefined) { const lastLine = lastNonemptyLine(formattedOutput); if (lastLine?.startsWith('ERROR: ')) { - await revealParserErrorLocation(document, lastLine); + const errorLocation = getJJParserErrorLocation(document, lastLine); + setJJParserErrorDiagnostic(prettyPrinterDiagnostics, document, errorLocation); + await revealJJParserErrorLocation(document, errorLocation); vscode.window.showErrorMessage(`\ Failed to format TPTP file: \ remote formatter provided by SystemB4TPTP exited with ${lastLine}`); @@ -488,7 +546,7 @@ export function activate(context: ExtensionContext) { } } - }) + }); context.subscriptions.push(formatProblem); @@ -1785,7 +1843,7 @@ export function activate(context: ExtensionContext) { } }); - }) + }); context.subscriptions.push(proveProblemMultiple); @@ -2122,7 +2180,7 @@ export function activate(context: ExtensionContext) { } } }) - }) + }); context.subscriptions.push(processSolution); @@ -2463,7 +2521,7 @@ export function activate(context: ExtensionContext) { } } }) - }) + }); context.subscriptions.push(processSolutionMultiple); @@ -2509,7 +2567,7 @@ export function activate(context: ExtensionContext) { } else { vscode.window.showInformationMessage('No problem selected.'); } - }) + }); context.subscriptions.push(importProblem); @@ -2556,7 +2614,7 @@ export function activate(context: ExtensionContext) { vscode.window.showInformationMessage('No Solution selected.'); } - }) + }); context.subscriptions.push(importSolution); From 2fae27fca446480eba6d7c50b6ac563d6e06ffff Mon Sep 17 00:00:00 2001 From: jzxia Date: Thu, 9 Jul 2026 15:47:45 +0800 Subject: [PATCH 09/14] refactor: move pretty-print command logic into dedicated folder; rename command from `tptp.formatProblem` to `tptp.prettyPrint` --- .../client/resources/wasm/tptp4X_wasm.d.ts | 2 +- tptplus/client/src/extension.ts | 238 +----------------- .../src/prettyPrint/jjParserDiagnostics.ts | 103 ++++++++ .../localPrettyPrint.ts} | 2 +- .../localPrettyPrintProcess.ts} | 4 +- .../src/prettyPrint/prettyPrintCommand.ts | 97 +++++++ tptplus/client/src/systemB4TptpOutput.ts | 42 ++++ tptplus/native/tptp-pretty/CMakeLists.txt | 2 +- tptplus/package.json | 4 +- 9 files changed, 257 insertions(+), 237 deletions(-) create mode 100644 tptplus/client/src/prettyPrint/jjParserDiagnostics.ts rename tptplus/client/src/{localPrettyPrinter.ts => prettyPrint/localPrettyPrint.ts} (96%) rename tptplus/client/src/{localPrettyPrinterProcess.ts => prettyPrint/localPrettyPrintProcess.ts} (96%) create mode 100644 tptplus/client/src/prettyPrint/prettyPrintCommand.ts create mode 100644 tptplus/client/src/systemB4TptpOutput.ts diff --git a/tptplus/client/resources/wasm/tptp4X_wasm.d.ts b/tptplus/client/resources/wasm/tptp4X_wasm.d.ts index ab716e4..d29901e 100644 --- a/tptplus/client/resources/wasm/tptp4X_wasm.d.ts +++ b/tptplus/client/resources/wasm/tptp4X_wasm.d.ts @@ -1,3 +1,3 @@ -declare const createTPTP4X: import('../../src/localPrettyPrinterProcess').CreateTPTP4X; +declare const createTPTP4X: import('../../src/prettyPrint/localPrettyPrintProcess').CreateTPTP4X; export = createTPTP4X; diff --git a/tptplus/client/src/extension.ts b/tptplus/client/src/extension.ts index f4976ee..b2f7c29 100644 --- a/tptplus/client/src/extension.ts +++ b/tptplus/client/src/extension.ts @@ -11,162 +11,17 @@ import { TransportKind } from 'vscode-languageclient/node'; -import { - createSystemB4TptpForm -} from './systemTptpForms'; -import { formatTptpLocally } from './localPrettyPrinter'; +import { createSystemB4TptpForm } from './systemTptpForms'; +import { registerPrettyPrintCommand } from './prettyPrint/prettyPrintCommand'; let client: LanguageClient; -interface JJParserErrorLocation { - position: vscode.Position; - range: vscode.Range; - message: string; - reportedText?: string; -} - -/** - * Extract the text between `
` and `
` from the HTML response of System B4 TPTP. - */ -function extractSystemB4TptpOutput(html: string): string | undefined { - const dom = new JSDOM(html); - const preText = dom.window.document.querySelector('pre')?.textContent ?? undefined; - if (preText === undefined) { - return undefined; - } - - const startMarker = '% START OF SYSTEM OUTPUT'; - const endMarker = '% END OF SYSTEM OUTPUT'; - const lines = preText.split('\n'); - const startLine = lines.findIndex(line => line.trim() === startMarker); - let endLine = -1; // TODO: use `findLastIndex`? - for (let i = lines.length - 1; i >= Math.max(0, startLine); i -= 1) { - if (lines[i].trim() === endMarker) { - endLine = i; - break; - } - } - - if (startLine === -1 || endLine === -1 || startLine >= endLine) { - return undefined; - } - - return lines.slice(startLine + 1, endLine).join('\n'); -} - -function lastNonemptyLine(text: string): string | undefined { - const lines = text.split('\n'); - for (let i = lines.length - 1; i >= 0; i -= 1) { - const line = lines[i].trim(); - if (line) { - return line; - } - } - - return undefined; -} - -/** - * Takes a JJParser error message and turns it into a VS Code location. - * @param message The expected message shape is like - * 'SyntaxError: Line 15 Char 6 Token "{" continuing with ...' or - * 'SyntaxError: Line 11 Char 42 Character "[" continuing with ...' - * @returns VS Code location or undefined - */ -function getJJParserErrorLocation(document: vscode.TextDocument, message: string): - JJParserErrorLocation | undefined -{ - const match = message.match(/\bLine\s+(\d+)\s+Char\s+(\d+)(?:\s+(?:Token|Character)\s+"([\s\S]*?)"\s+continuing\b)?/); - if (!match) { - return undefined; - } - - const reportedLine = Number.parseInt(match[1], 10); - const reportedCharacter = Number.parseInt(match[2], 10); - if (Number.isNaN(reportedLine) || Number.isNaN(reportedCharacter)) { - return undefined; - } - - const lineIndex = Math.max(0, Math.min(reportedLine - 1, document.lineCount - 1)); - const lineText = document.lineAt(lineIndex).text; - let characterIndex = Math.max(0, Math.min(reportedCharacter - 1, lineText.length)); - const reportedText = match[3]; - - // If the error message reports a token or character, try to move cursor to its beginning. - if (reportedText) { - const reportedTextIndex = lineText.slice(0, characterIndex + 1).lastIndexOf(reportedText); - if (reportedTextIndex >= 0) { - characterIndex = reportedTextIndex; - } - } - - const startPosition = new vscode.Position(lineIndex, characterIndex); - const endCharacterIndex = reportedText - ? Math.min(lineText.length, characterIndex + reportedText.length) - : characterIndex; - const endPosition = new vscode.Position(lineIndex, endCharacterIndex); - - return { - position: startPosition, - range: new vscode.Range(startPosition, endPosition), - message: message, - reportedText: reportedText - }; -} - -/** - * Adds a warning diagnostic for a JJParser-reported token or character. - * The squiggle and diagnostic message are cleared on document edit or before - * each new pretty-printer run. - */ -function setJJParserErrorDiagnostic( - diagnostics: vscode.DiagnosticCollection, - document: vscode.TextDocument, - errorLocation: JJParserErrorLocation | undefined -) { - if (!errorLocation?.reportedText) { - return; - } - - const diagnostic = new vscode.Diagnostic( - errorLocation.range, - errorLocation.message, - vscode.DiagnosticSeverity.Warning - ); - diagnostic.source = 'TPTP pretty-printer (JJParser)'; - diagnostics.set(document.uri, [diagnostic]); -} - -/** - * Takes a JJParser error location and, if it points to a specific position in source file, - * highlight the position. - * @param errorLocation The location parsed from a JJParser error message. - */ -async function revealJJParserErrorLocation( - document: vscode.TextDocument, - errorLocation: JJParserErrorLocation | undefined -): Promise -{ - const position = errorLocation?.position; - if (!position) { - return; - } - - const range = new vscode.Range(position, position); - const editor = await vscode.window.showTextDocument(document, { - preview: false, - selection: range, - }); - editor.selection = new vscode.Selection(position, position); - editor.revealRange(range, vscode.TextEditorRevealType.InCenterIfOutsideViewport); -} - export function activate(context: ExtensionContext) { - const prettyPrinterDiagnostics = vscode.languages.createDiagnosticCollection('tptpPrettyPrinter'); - context.subscriptions.push(prettyPrinterDiagnostics); + const prettyPrintDiagnostics = vscode.languages.createDiagnosticCollection('tptpPrettyPrint'); + context.subscriptions.push(prettyPrintDiagnostics); context.subscriptions.push( vscode.workspace.onDidChangeTextDocument(event => { - prettyPrinterDiagnostics.delete(event.document.uri); + prettyPrintDiagnostics.delete(event.document.uri); }) ); @@ -469,86 +324,9 @@ export function activate(context: ExtensionContext) { context.subscriptions.push(prepareProblem); //@ FORMAT A PROBLEM BY RUNNING JJPARSER LOCALLY, USING REMOTE SYSTEMB4TPTP AS FALLBACK - const formatProblem = vscode.commands.registerCommand('tptp.formatProblem', async (uri: vscode.Uri) => { - if (!uri) { - const activeEditor = vscode.window.activeTextEditor; - if (!activeEditor) { - vscode.window.showErrorMessage('No active TPTP file open'); - return; - } - uri = activeEditor.document.uri; - } - - // Clear stale parser diagnostics before each new pretty-printer run. - prettyPrinterDiagnostics.delete(uri); - - const document = await vscode.workspace.openTextDocument(uri); - const sourceText = document.getText(); - const fullTextRange = new vscode.Range( - document.positionAt(0), - document.positionAt(sourceText.length) - ); - - // use WorkspaceEdit to edit any URI's document, even if it's invisible - const edit = new vscode.WorkspaceEdit(); - - // a whitespace-only file should become empty - if (!sourceText.trim()) { - edit.replace(uri, fullTextRange, ""); - await vscode.workspace.applyEdit(edit); - return; - } - - // call the local pretty-printer (JJParser) - const localResult = await formatTptpLocally(context, sourceText); - if (localResult.kind === 'success') { - edit.replace(uri, fullTextRange, localResult.output); - await vscode.workspace.applyEdit(edit); - return; - } - if (localResult.kind === 'parser-error') { - const errorLocation = getJJParserErrorLocation(document, localResult.message); - if (errorLocation !== undefined) { - setJJParserErrorDiagnostic(prettyPrinterDiagnostics, document, errorLocation); - await revealJJParserErrorLocation(document, errorLocation); - vscode.window.showErrorMessage(`Failed to format TPTP file: ${localResult.message}`); - return; - } else { - vscode.window.showWarningMessage(`\ - Failed to format TPTP file locally: ${localResult.message} - Trying the remote formatter provided by SystemB4TPTP...`); - } - } - - // Fall back to remote pretty-printer if the local pretty-printer fails on an unknown error - // or an error that does not point to any specific location in `sourceText`. - const form = createSystemB4TptpForm(sourceText, null); - const response = await fetch('https://tptp.org/cgi-bin/SystemOnTPTPFormReply', { - method: 'POST', - body: form - }); - const text = await response.text(); - const formattedOutput = extractSystemB4TptpOutput(text); - - if (formattedOutput !== undefined) { - const lastLine = lastNonemptyLine(formattedOutput); - if (lastLine?.startsWith('ERROR: ')) { - const errorLocation = getJJParserErrorLocation(document, lastLine); - setJJParserErrorDiagnostic(prettyPrinterDiagnostics, document, errorLocation); - await revealJJParserErrorLocation(document, errorLocation); - vscode.window.showErrorMessage(`\ - Failed to format TPTP file: \ - remote formatter provided by SystemB4TPTP exited with ${lastLine}`); - } else { - edit.replace(uri, fullTextRange, formattedOutput); - await vscode.workspace.applyEdit(edit); - vscode.window.showInformationMessage("Format TPTP file successful."); - } - } - - }); - - context.subscriptions.push(formatProblem); + context.subscriptions.push( + registerPrettyPrintCommand(context, prettyPrintDiagnostics) + ); //@ RUN A THEOREM THROUGH SYSTEMONTPTP const proveProblem = vscode.commands.registerCommand('tptp.proveProblem', async (uri: vscode.Uri) => { diff --git a/tptplus/client/src/prettyPrint/jjParserDiagnostics.ts b/tptplus/client/src/prettyPrint/jjParserDiagnostics.ts new file mode 100644 index 0000000..189813b --- /dev/null +++ b/tptplus/client/src/prettyPrint/jjParserDiagnostics.ts @@ -0,0 +1,103 @@ +import * as vscode from "vscode"; + +export interface JJParserErrorLocation { + position: vscode.Position; + range: vscode.Range; + message: string; + reportedText?: string; +} + +/** + * Takes a JJParser error message and turns it into a VS Code location. + * @param message The expected message shape is like + * 'SyntaxError: Line 15 Char 6 Token "{" continuing with ...' or + * 'SyntaxError: Line 11 Char 42 Character "[" continuing with ...' + * @returns VS Code location or undefined + */ +export function getJJParserErrorLocation(document: vscode.TextDocument, message: string): + JJParserErrorLocation | undefined +{ + const match = message.match(/\bLine\s+(\d+)\s+Char\s+(\d+)(?:\s+(?:Token|Character)\s+"([\s\S]*?)"\s+continuing\b)?/); + if (!match) { + return undefined; + } + + const reportedLine = Number.parseInt(match[1], 10); + const reportedCharacter = Number.parseInt(match[2], 10); + if (Number.isNaN(reportedLine) || Number.isNaN(reportedCharacter)) { + return undefined; + } + + const lineIndex = Math.max(0, Math.min(reportedLine - 1, document.lineCount - 1)); + const lineText = document.lineAt(lineIndex).text; + let characterIndex = Math.max(0, Math.min(reportedCharacter - 1, lineText.length)); + const reportedText = match[3]; + + // If the error message reports a token or character, try to move cursor to its beginning. + if (reportedText) { + const reportedTextIndex = lineText.slice(0, characterIndex + 1).lastIndexOf(reportedText); + if (reportedTextIndex >= 0) { + characterIndex = reportedTextIndex; + } + } + + const startPosition = new vscode.Position(lineIndex, characterIndex); + const endCharacterIndex = reportedText + ? Math.min(lineText.length, characterIndex + reportedText.length) + : characterIndex; + const endPosition = new vscode.Position(lineIndex, endCharacterIndex); + + return { + position: startPosition, + range: new vscode.Range(startPosition, endPosition), + message: message, + reportedText: reportedText + }; +} + +/** + * Adds a warning diagnostic for a JJParser-reported token or character. + * The squiggle and diagnostic message are cleared on document edit or before + * each new pretty-printer run. + */ +export function setJJParserErrorDiagnostic( + diagnostics: vscode.DiagnosticCollection, + document: vscode.TextDocument, + errorLocation: JJParserErrorLocation | undefined +) { + if (!errorLocation?.reportedText) { + return; + } + + const diagnostic = new vscode.Diagnostic( + errorLocation.range, + errorLocation.message, + vscode.DiagnosticSeverity.Warning + ); + diagnostic.source = 'TPTP pretty-printer (JJParser)'; + diagnostics.set(document.uri, [diagnostic]); +} + +/** + * Takes a JJParser error location and, if it points to a specific position in source file, + * highlight the position. + * @param errorLocation The location parsed from a JJParser error message. + */ +export async function revealJJParserErrorLocation( + document: vscode.TextDocument, + errorLocation: JJParserErrorLocation | undefined +): Promise +{ + const position = errorLocation?.position; + if (!position) { + return; + } + + const range = new vscode.Range(position, position); + const editor = await vscode.window.showTextDocument(document, { + preview: false, + selection: range, + }); + editor.selection = new vscode.Selection(position, position); + editor.revealRange(range, vscode.TextEditorRevealType.InCenterIfOutsideViewport); +} diff --git a/tptplus/client/src/localPrettyPrinter.ts b/tptplus/client/src/prettyPrint/localPrettyPrint.ts similarity index 96% rename from tptplus/client/src/localPrettyPrinter.ts rename to tptplus/client/src/prettyPrint/localPrettyPrint.ts index a56f5b8..b247d2c 100644 --- a/tptplus/client/src/localPrettyPrinter.ts +++ b/tptplus/client/src/prettyPrint/localPrettyPrint.ts @@ -2,7 +2,7 @@ import { spawn } from 'child_process'; import * as path from 'path'; import * as vscode from 'vscode'; -const RUNNER_PATH = path.join('client', 'out', 'localPrettyPrinterProcess.js'); +const RUNNER_PATH = path.join('client', 'out', 'prettyPrint', 'localPrettyPrintProcess.js'); const LOCAL_PRETTY_PRINT_TIMEOUT_MS = 10000; // TODO: make this configurable export type LocalPrettyPrintResult = diff --git a/tptplus/client/src/localPrettyPrinterProcess.ts b/tptplus/client/src/prettyPrint/localPrettyPrintProcess.ts similarity index 96% rename from tptplus/client/src/localPrettyPrinterProcess.ts rename to tptplus/client/src/prettyPrint/localPrettyPrintProcess.ts index 7f7ff6b..94150f4 100644 --- a/tptplus/client/src/localPrettyPrinterProcess.ts +++ b/tptplus/client/src/prettyPrint/localPrettyPrintProcess.ts @@ -1,8 +1,8 @@ import * as fs from 'fs'; import * as path from 'path'; -import createTPTP4X from '../resources/wasm/tptp4X_wasm.js'; +import createTPTP4X from '../../resources/wasm/tptp4X_wasm.js'; -const WASM_DIR = path.join(__dirname, '..', 'resources', 'wasm'); +const WASM_DIR = path.join(__dirname, '..', '..', 'resources', 'wasm'); const WASM_BIN_PATH = path.join(WASM_DIR, 'tptp4X_wasm.wasm'); export type TPTP4XModule = { diff --git a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts new file mode 100644 index 0000000..0aa2efb --- /dev/null +++ b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts @@ -0,0 +1,97 @@ +import * as vscode from "vscode"; + +import { + getJJParserErrorLocation, + revealJJParserErrorLocation, + setJJParserErrorDiagnostic +} from './jjParserDiagnostics'; +import { formatTptpLocally } from './localPrettyPrint'; +import { createSystemB4TptpForm } from '../systemTptpForms'; +import { + extractSystemB4TptpOutput, + lastNonemptyLine +} from '../systemB4TptpOutput'; + +export function registerPrettyPrintCommand( + context: vscode.ExtensionContext, + prettyPrintDiagnostics: vscode.DiagnosticCollection +): vscode.Disposable { + return vscode.commands.registerCommand('tptp.prettyPrint', async (uri: vscode.Uri) => { + if (!uri) { + const activeEditor = vscode.window.activeTextEditor; + if (!activeEditor) { + vscode.window.showErrorMessage('No active TPTP file open'); + return; + } + uri = activeEditor.document.uri; + } + + // Clear stale parser diagnostics before each new pretty-printer run. + prettyPrintDiagnostics.delete(uri); + + const document = await vscode.workspace.openTextDocument(uri); + const sourceText = document.getText(); + const fullTextRange = new vscode.Range( + document.positionAt(0), + document.positionAt(sourceText.length) + ); + + // use WorkspaceEdit to edit any URI's document, even if it's invisible + const edit = new vscode.WorkspaceEdit(); + + // a whitespace-only file should become empty + if (!sourceText.trim()) { + edit.replace(uri, fullTextRange, ""); + await vscode.workspace.applyEdit(edit); + return; + } + + // call the local pretty-printer (JJParser) + const localResult = await formatTptpLocally(context, sourceText); + if (localResult.kind === 'success') { + edit.replace(uri, fullTextRange, localResult.output); + await vscode.workspace.applyEdit(edit); + return; + } + if (localResult.kind === 'parser-error') { + const errorLocation = getJJParserErrorLocation(document, localResult.message); + if (errorLocation !== undefined) { + setJJParserErrorDiagnostic(prettyPrintDiagnostics, document, errorLocation); + await revealJJParserErrorLocation(document, errorLocation); + vscode.window.showErrorMessage(`Failed to format TPTP file: ${localResult.message}`); + return; + } else { + vscode.window.showWarningMessage(`\ + Failed to format TPTP file locally: ${localResult.message} + Trying the remote formatter provided by SystemB4TPTP...`); + } + } + + // Fall back to remote pretty-printer if the local pretty-printer fails on an unknown error + // or an error that does not point to any specific location in `sourceText`. + const form = createSystemB4TptpForm(sourceText, null); + const response = await fetch('https://tptp.org/cgi-bin/SystemOnTPTPFormReply', { + method: 'POST', + body: form + }); + const text = await response.text(); + const formattedOutput = extractSystemB4TptpOutput(text); + + if (formattedOutput !== undefined) { + const lastLine = lastNonemptyLine(formattedOutput); + if (lastLine?.startsWith('ERROR: ')) { + const errorLocation = getJJParserErrorLocation(document, lastLine); + setJJParserErrorDiagnostic(prettyPrintDiagnostics, document, errorLocation); + await revealJJParserErrorLocation(document, errorLocation); + vscode.window.showErrorMessage(`\ + Failed to format TPTP file: \ + remote formatter provided by SystemB4TPTP exited with ${lastLine}`); + } else { + edit.replace(uri, fullTextRange, formattedOutput); + await vscode.workspace.applyEdit(edit); + vscode.window.showInformationMessage("Format TPTP file successful."); + } + } + + }); +} diff --git a/tptplus/client/src/systemB4TptpOutput.ts b/tptplus/client/src/systemB4TptpOutput.ts new file mode 100644 index 0000000..894a727 --- /dev/null +++ b/tptplus/client/src/systemB4TptpOutput.ts @@ -0,0 +1,42 @@ +import { JSDOM } from 'jsdom'; + +/** + * Extract the text between `
` and `
` from the HTML response of System B4 TPTP. + */ +export function extractSystemB4TptpOutput(html: string): string | undefined { + const dom = new JSDOM(html); + const preText = dom.window.document.querySelector('pre')?.textContent ?? undefined; + if (preText === undefined) { + return undefined; + } + + const startMarker = '% START OF SYSTEM OUTPUT'; + const endMarker = '% END OF SYSTEM OUTPUT'; + const lines = preText.split('\n'); + const startLine = lines.findIndex(line => line.trim() === startMarker); + let endLine = -1; // TODO: use `findLastIndex`? + for (let i = lines.length - 1; i >= Math.max(0, startLine); i -= 1) { + if (lines[i].trim() === endMarker) { + endLine = i; + break; + } + } + + if (startLine === -1 || endLine === -1 || startLine >= endLine) { + return undefined; + } + + return lines.slice(startLine + 1, endLine).join('\n'); +} + +export function lastNonemptyLine(text: string): string | undefined { + const lines = text.split('\n'); + for (let i = lines.length - 1; i >= 0; i -= 1) { + const line = lines[i].trim(); + if (line) { + return line; + } + } + + return undefined; +} diff --git a/tptplus/native/tptp-pretty/CMakeLists.txt b/tptplus/native/tptp-pretty/CMakeLists.txt index 6ae4b11..8a49688 100644 --- a/tptplus/native/tptp-pretty/CMakeLists.txt +++ b/tptplus/native/tptp-pretty/CMakeLists.txt @@ -1,6 +1,6 @@ cmake_minimum_required(VERSION 3.18) -project(TPTPPrettyPrinter LANGUAGES C) +project(TPTPPrettyPrint LANGUAGES C) # provide clues to IDE IntelliSense set(CMAKE_EXPORT_COMPILE_COMMANDS ON) diff --git a/tptplus/package.json b/tptplus/package.json index c4ffe45..6036486 100644 --- a/tptplus/package.json +++ b/tptplus/package.json @@ -55,7 +55,7 @@ "title": "TPTP: Prepare Problem" }, { - "command": "tptp.formatProblem", + "command": "tptp.prettyPrint", "title": "TPTP: Format TPTP File" }, { @@ -91,7 +91,7 @@ "group": "navigation" }, { - "command": "tptp.formatProblem", + "command": "tptp.prettyPrint", "when": "editorLangId == tptp", "group": "navigation" }, From 6cc482813ccbd329ac4e4f731ac3c45420788a17 Mon Sep 17 00:00:00 2001 From: jzxia Date: Thu, 9 Jul 2026 15:54:33 +0800 Subject: [PATCH 10/14] mark command "TPTP: Format Document" as legacy, preferring "TPTP: Format TPTP File" --- tptplus/package.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tptplus/package.json b/tptplus/package.json index 6036486..3d9a1b6 100644 --- a/tptplus/package.json +++ b/tptplus/package.json @@ -48,7 +48,7 @@ "commands": [ { "command": "tptp.formatDocument", - "title": "TPTP: Format Document" + "title": "TPTP: Format Document (legacy)" }, { "command": "tptp.prepareProblem", From 5bf601e7b8dd66c5591f3096497297757b5f1858 Mon Sep 17 00:00:00 2001 From: jzxia Date: Thu, 9 Jul 2026 16:20:28 +0800 Subject: [PATCH 11/14] feat: add button in the editor title menu that runs command "TPTP: Check Syntax and Format TPTP File"; move icons into `images/icons` --- tptplus/images/icons/Syntax.png | Bin 0 -> 7750 bytes tptplus/images/{ => icons}/TPTPWorld.png | Bin tptplus/images/{ => icons}/TPTPWorld.svg | 0 tptplus/package.json | 19 +++++++++++++++---- 4 files changed, 15 insertions(+), 4 deletions(-) create mode 100644 tptplus/images/icons/Syntax.png rename tptplus/images/{ => icons}/TPTPWorld.png (100%) rename tptplus/images/{ => icons}/TPTPWorld.svg (100%) diff --git a/tptplus/images/icons/Syntax.png b/tptplus/images/icons/Syntax.png new file mode 100644 index 0000000000000000000000000000000000000000..6b12f2a3eaed132b2bb4379de1e2ca5a005c949f GIT binary patch literal 7750 zcmeHL2~<<(wmz8%V-i3`fdE30w$>Qt03t*{u*!_g3Xw@PB!`3;K!yZFwCz=Ct0)4B z6CqSY>npJeBw`<0s;v^N1H<8}phpB+%?*V@?#V#4_ubp|?py1%_pbM{$jUz7-uv78 z?0^6J{D-{}VZkPbmWBWTn5+v4i~;~uKk^;c*F%tN!NlFjj{z8xzy$y!bM+Sm)YL9U zgvWV7@p%F4oSY0+9*~otna#}bc61HUN{%knt!!?dqidj}i%SqQBQ1}^W+5VibJG~i z46VXhi)>+Y(la<(h^mHMgB+=J#8my~8jzmN$l@?^kP8+gN9P&A$jVrubI(rKx^iPP zqrx_^MQ0GY9KnhaQ!GMdHy!kija)#tgX7xGS!a z(wOSr1R1aCbP>3D1@rB?BZHHdjZ}IAV@n1zg3Zm&%SM{oHE;_%FOQw$=(=X!fX>X$ zQY-S^#^ID zf9;lWq5h#QRto;qKu|p}EuCJ)J$M9&RqWTE8(AcCyc9y7Wrkqcngh9{`h2KJeVFxEY=fq6kk^MJB8fq9*A+dW$)I z0ai9MWGOQ|06b#*Y(JA`I#YEfr>rzfhAzM&JBdoM z`8g4oN+26zl{xIoa{y$_14#Wf5IQAxzt2wC^HK;XEERVjecm)QW-r5)i10N#n}%N6 z%PIoom~RqbWk(1&oC!BnOu#2dQMXacnU4F2 z*x6KRIDWk2QBYaW4=|(5M?6tj1#xN%_dr-h9da}KBK8w&&vg8R=vVZmVH%q~QxUz9 zLIQM(JsF6Ypg0bc#!htE%brBRrYM_e_E+|@j6`2cDHnc$b2t~+ z+&uVcP}%x3Hdv?_E>3t$Qk3kAmCp3}eE!r*+a-OG?_>Nm1y3Yl4=y$jy~E}|Ke_Ka zS3-5Q=n)7-t!xGmeh zvgerG8S{Ccm3vj!6AJH|)Dk{hbA6ceiTCEz6^hKz$KWOLzD4oT?VHTKk}2Xe+}&9A zJ%nH-93u3UCwU-Vo5)VB)rGywIFicdli0t+upb5zl&QP}(hj)z==EV65yA9cN;}uw ztG`Qbip~-4b+x9m`u#~*nM(D5RP-@mmB?^Uc`NFxB@lRG+jb5>t`sg0^dgtE$_(feNKdIiLR|u=}x(Fmr0qAXf;8ar3i&=u>6SP zWT*um7`cz-Zzw(hZG-D7Cd~Ss6+e_MR8X#7HW)uJEtS2aXra@=U^$*NczVz=-cjNJ zI~bf3DRC_!AYR^W-XZ3r$2H=?QL(Bx-%NJaHWhlxVJrLyKRZek7-Q@7@rJo-p~}2} z8l^{Y|2|sPCVh@=v!0U(_(f#3DQI@aRr2DPHF5J1GQw>9e$?L&Sx>nMD z><^eei|#b`bK@KPQs>5>+d9o_6NyPfI#jBj$qy#E#2aG&c;NGJc^5$KFX1h{MI zEHM>dmSk7V9Nst`F8u)8=07dDy5w0Yn(riWywkm)qiW6*bSg`-FQyHr+$l9kG+lxpEcQosGPE`9SmD&r_@+lJ}IS1-OgR{l;|(%Z$r(syQ6(7VV~S3isTe8R9) z5)K*bHK`T){zVu4AG$7#Vcn=H(Njk7UO@{KE3UGgC6!_aypwpsteyc9W4lel;)dS- zd6&#Lnd~MBDsG-!SiV!@y#+iu%^G&lQ=)lSpiIT=)#c?o_j)H%gNl2`GQgElm4;`U z*fpDs$1`AmS)gLm=jF2Y2(r`R&pOy6E|O~TNvxHef9pLx5Yx$@f}V zz^JpNyibNQUdc8dNAp0S>qFV5llx32BiaP5T?)+9DACW3CKw*L4pCw%_3}kYQopvg z5@2}LmSioRWHG=SX_!^=70~{qBtHRHejfGFc)DISABKS4eEagAO86eImTy_!)2KlV z%X`}TZVPY1Gou!kiGG3^`LOUT{BYE3<$R$zXu77*iG&aANcx9TUW7GP%`JW@CMVa& zcH@_c`QIAd{LEJRLm#SaFFf!vaQSn5>ppLPYG`|bhsT8yV7oW~8!b=D3a~&FUwE&j z(%ZQ`&{NoidwRP91J!#cgMkXxr8^gB{o0Bg#mjG8z5G=lGF|o}BZ($QtX@(58J23>xmE#1bRVN2;s>OBW$a^OSdjbiRB04!v z62snNkGHVrfk)2Hsm#43tq#0hM^4X8^wK0Cz&o4}J$tS(7aW$tsoWxkZT&S_1+LF@ zlm>Tt?=3g#k_)p^U=s?X* z9ji+?i>XL57RyH?9;fzUPwcdk;cO!D7@2P!gx=r$NC?%dk1BE9SedU7LbKz#ak9|y zjuN0XiEN1+ZrV2c0Z=r#?k4=glavgF@B|)W&tqYr@KN8=2PXy#yk)qSsNn1ig%6)$ zEhJIo#=UT8qj@s4jdyBUQ(G-!_*~AY5fAdzhLL!+p$XQ4mPkIa0HaOW(Ly5IX5sye7jnp4)K$-m5d%>O; zE3g(*2fYdU<7W{emW;vj4Q03vkzXm6|E{d!D|mnX=Hl|B`jqz~OUG)PI(kB}7J6d8 z-0{dEcv+cIb+aFHeB;o#2O^66vPPQNg-7Ry$og#|C{!s`vIT-=KK4K%B z z$zo@eEp-!lu^>)9aO0qF6Y+2h!9*I%V{_8NVa%E4a!hN`z>)s@pG*s$!IQwM=JEA5 zV;X+}P#?*64A)-l0c@Ife(asH!iC;~s8?T;h%a{PukyfG9vP%)-;S&F$E%eV8L&f?)dhH2H$Mk)|S~l(t!u$ZoKkTvGmKoxT5*n_*NBK z&8N~$59-$DYJHr*${p3Wv%qM7%zne#<^jeSRZU!pyColA`NiV?1>Z?~(OKEbMMsTU zhFhTmVeyNWEyrY`D3et#t<3|GwO!B|fu4=!z25OF0`1LwA=BUE6*@5~kCYtnezPLeRwJshnuIskdR=-jQRiR?s6n5kq`sEHOVsy#LP zdF$8ez=p=L|DiGu`%$|z{q!(o(_rays%ZT=$S|%vvhRK3-O?KXGBU9?H}xKAuc@IH5PSPVL=o zUh?_uY5{WIaEp*dR=nT?SHd*-As=Sxb7__V%Tff9URpmKa%~OPgsb5)OV9bQl!amz zTIUurOZQ7JVLeS^z{jT1P?4HnAGOA?He78h^A8lhR5RF7!rNx8FdIln6#9X%^Rr1P zH+4k%b*!1j$!s++=ntY&1<1=LAj1hzWkvu7YXRu#QvhR9GO*ZA0#N4-1m|9;MvZ{# zcohbK^q!Xjz^Xyr`TSq`ZT|mSZbcKC|FB?y4&T<&ILRaRGXPi@6c*UBCbjIZ6rLA6 literal 0 HcmV?d00001 diff --git a/tptplus/images/TPTPWorld.png b/tptplus/images/icons/TPTPWorld.png similarity index 100% rename from tptplus/images/TPTPWorld.png rename to tptplus/images/icons/TPTPWorld.png diff --git a/tptplus/images/TPTPWorld.svg b/tptplus/images/icons/TPTPWorld.svg similarity index 100% rename from tptplus/images/TPTPWorld.svg rename to tptplus/images/icons/TPTPWorld.svg diff --git a/tptplus/package.json b/tptplus/package.json index 3d9a1b6..97418a8 100644 --- a/tptplus/package.json +++ b/tptplus/package.json @@ -4,7 +4,7 @@ "publisher": "TPTPWorld", "description": "Syntax highlighting, error detection, pretty-printing, and proving & processing theorems functions for TPTP language", "version": "0.1.10", - "icon": "images/TPTPWorld.png", + "icon": "images/icons/TPTPWorld.png", "repository": { "type": "git", "url": "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/TPTPWorld/VSCodeExtension" @@ -33,8 +33,8 @@ ], "configuration": "./language-configuration.json", "icon": { - "light": "./images/TPTPWorld.svg", - "dark": "./images/TPTPWorld.svg" + "light": "./images/icons/TPTPWorld.svg", + "dark": "./images/icons/TPTPWorld.svg" } } ], @@ -56,7 +56,11 @@ }, { "command": "tptp.prettyPrint", - "title": "TPTP: Format TPTP File" + "title": "TPTP: Check Syntax and Format TPTP File", + "icon": { + "light": "./images/icons/Syntax.png", + "dark": "./images/icons/Syntax.png" + } }, { "command": "tptp.proveProblem", @@ -84,6 +88,13 @@ } ], "menus": { + "editor/title": [ + { + "command": "tptp.prettyPrint", + "when": "editorLangId == tptp", + "group": "navigation" + } + ], "editor/context": [ { "command": "tptp.prepareProblem", From 3c05401f70f43be55c5e3dea7908cdc9a90fee4d Mon Sep 17 00:00:00 2001 From: jzxia Date: Thu, 9 Jul 2026 19:28:21 +0800 Subject: [PATCH 12/14] feat: detect duplicate TPTP formula names in local pretty-printer --- .../client/resources/wasm/tptp4X_wasm.wasm | Bin 147060 -> 151190 bytes .../src/prettyPrint/localPrettyPrint.ts | 1 + .../prettyPrint/localPrettyPrintProcess.ts | 5 +++ .../src/prettyPrint/prettyPrintCommand.ts | 38 ++++++++++++------ .../src/prettyPrint/prettyPrintErrors.ts | 6 +++ tptplus/native/tptp-pretty/src/tptp4X_api.c | 29 +++++++++++++ 6 files changed, 67 insertions(+), 12 deletions(-) create mode 100644 tptplus/client/src/prettyPrint/prettyPrintErrors.ts diff --git a/tptplus/client/resources/wasm/tptp4X_wasm.wasm b/tptplus/client/resources/wasm/tptp4X_wasm.wasm index 1203f0b940aac047afc606c1b26f76d09a32400a..915ceef277deb190bc8ca28c6330bd94533f1fd5 100755 GIT binary patch delta 30467 zcmdVDcVJaT^FMs&+?M3tkOL&7lI%%=gq9E>bjYE1kS;1kqy?k~>?Bm_pog%aNU_kQ z2MAq|BB&@emOmPf}?KuL(!5#9prM6Gt}X9IUJgUf%)*C z`g3Ypn5F?T{u~ac<^fRkhdxo@@;N9BO~~cb9AR8Z{Q->qQo$P$YF*Y6-9DGg<+I8- z)99*I+u1F8msT!+bpGhtPxc!;cF>@HlJvMAqzd=t9%XfTD5&ilN9zSy6xPGHX+F9>vQG*^IH*oB*(fNZ$ zqV9l!!}|>ziMmIvELXIL`*FO3*91Cdb#%oS9M?isrEUWz400UO{3_9P(760jV+T17 zYhfyFjsOavvj4HCMm8TXVnn~ZVR^$G?`xsU3PF8xnB?=%&}M40w9E7(U80|8f%by7 zN!zRyYhk-i%-|Ucap*@ieV*pq5<-)xAjM&jDGXWv35t8s-5^vL;leM%^?g=zcb9^d zWW)%kh{@6X`fFsw;ypG;3(?;uBM$FzIhxBPBVNSouafC75=4SN0MCk|qW(I?p(s%# z>W4@;)3rz=$&4|CND?B?FzlRUGr>p^$s#4sNEL=i)t}dlG`pyhs3g)Na^7oJy5=z2nq`c3qOEAB?tu~=qw7lj58jkLZ)Gg%}T^zlX&`#v|fkqpx^G^lfGILm&M`Khb}TF+j@|16qbV z{7#>67BFca6_4sZV<7Se2C_N#F;h1NVVVZz8H2@OV~BW64AK3@P*fXwU$tRoh><6T ziM%{xxQ)dKF@jNjTnrbF>$Ax3@Hx;EgB&SF@?(@3rGH7rXh13$4NUC9F~EAP7$e4F z+WZt~F%FseVw}h?oy+lJe7Y86OaNvRa1@C{W!;hzRB-U6c{J z{vH`+L4dM>@w<$2=%XA)WNxoxlo#cNQ=g;70brzvOxMoWF``72{uRW+VN^iP3gA$` zrf>`~qD?;}En39nv5@iL)EGmIc+6pfh!gkE#6h%PQKa=lm_hxm5MLwLW*2p`KB}2)<@t(fmX+vlMIT#({Oux&>?!sebwnL7 zg|*+GT@YzB5lz4vae+B(Dw;CEaxrF8^3Q*B+w8p5~ zh}NP_p3zpc)sF^yX(!q-+q4($^<5ed*AJ2GfOj7T-4O)sm}i7_5}i^V5xxfG0m^B# z%jzCJl#W>Y!snB;I+m%7-|=N0r3mYEnat`N38*_o9iFmPwT&E+Epjkv^D$|5=a*N<4WBMKFy=WFW`Mn&^*8kAc_sJ9}`NYZjKgrvX_7KdOu1S%QkXEp8V z(2K0mdTm-_y`eYdZZiQqle_&e+sG2tL{@3HHBnMC&&U?pMlDeb-Igs|#q}{!1#5Fi z)pB|{!=w80a9`k9m!!s&Y;AtiGfeSs8BvDWI6}Atl&9h^t_6-&#brfVE-oi@QBIdy zoB{z}b&2v^8(hNN>JpJi`MA(;M1d9+kX0eih!)Y1oG5w5O;xD8)iF1YBIOt5sFCXu zkzgJvz@)lS*{w$#9=v;n*9ZY=JhqDP8=Zl{K+%!{gDeKQ$7QMV^^ z!O0jb3*AI7;R-NcZ%*zqb#VV$kYl{!h~Y9QBX%wV?dlptnU>9%;V=7Wy#f=WN0F(_-0fIdCu0r#C&OO zj~*HKei{br5nd6Z?;#^pFLabjF$pxp>J!r_;Yc)C1R4#?VYDbGBANV9WEDht zeV(;7rjvh37M6Rg`ohrnSpL`qDzP$Ro2ETwRE3_cnxhF`D%|N>x={_xQQcgS1tL}x z)kO{cEo*LUlavXNQa4Mf2-M3#e|1eO3&NQr>WX@R`%7#E9T|;81JO`4(htHq7->bu z4Wc;f>A0Et$M;6UMWd|p@sDQ2G2^Fesmw;q|4N{$1xAChN83Zu4_eFO+ZH5YU2q8x zEFN1fyr#zpF&9M}p-dnV%6-};VL;Dk{$3Nz9R`&B_e#Ri#%Aw*WY>*AT}&BPlM<{Z zESBe)w#Ri#FUOTliP#@_&eU} zQZb?VS2ZzTwM1=E=N?w}jLo_?V|(q9xQzOczXl*|gFK_5Xb8coAK|-eZK_!9zYzSr z)c=1Iyzc);f?G9`46Tr?E=dWMK;gQg4)gv!3fIFF)i*)m2BMy*FB<53trwF_ddK=S zDIaR1t@wzJTJc6h&&3R*oVn9_*hof3fiaSXS-%)rG~7x`ZlKSrjFoL?3bbNfnCq{l zS$B6NSksczQE6jxPUT@Xht#wuJzLZi*}A|4*1`nV$}?(<+PwJgvwSI?T3#<#I#Ey_ zVM=*~1r$#s$cM-9o2V1c5`z5(I0_>u13+aU=y-*xr6*a-Qd0b%L_rA3L4id=&`+eq za7K($GBJ?N-%=te$?~M8v^*CDzQ&3S-bRl?^(abvG|*$Ri8?84AHgQ#9yKEsJ*IMx zyz@vyk0Vo4{J%#TRahuQ74-N@Y7A$Tvc7dNm3#agJ+6r=Wp(tJqk7CK?XfO;tY@N5 zeO6MiA-G4U&F$QylQ|weHc3k{4n<)P(?m4IK89<#VJ*3M4NdI;4@&71g@2 zPRiwyhvoCyRfo)|aS~vf(OQFPJgd3a#)(S#Oz@ zi+9yHN>t4%%z77O$*LViRjmOvt5S7qZp~qorJB@KO|mV$P7KwO2eV=RG^tbBD$G7l znfEoUp&DkXhP740I;vrgYFIbeunTpwjQR=I*`^+=dHwiw7qmjSUOj+u1Pre-OmAiK z!y;s>6icOE-Ky9i#`5QM#Qwynp9}<_%MtipmQzAqP}ayw$<45S&yCacTx)3VqgMTT z?JKr{>TxKuGaM7?3&0J5<|(5$v{u%OrG~0$R!&9$Y?cC>rNBN=T(N;u16hnl2_Q?8 zMl11t7VkBzzZ<=cz7I5J48BvpT9ZxGI5;q>Z}n|D=)QD=e@iz+T49WuY*{w}%Co^& z9dl!?aC0ctQ@ITk{h9{ms!N#&!)>0)3~X78tcuOzfl&Qsc1KCp{$^9CMRBv{y9hns zZqbigSr50Iir?>AR-@K7{Zm?v{a>llOi`toqDn~X|DA#jRNV%u?$Or6!C+suSxuGI zZ#sS(S^L{&PyZ!{)?P`CCy5hHwb-P14)wa?)?nCamj*@zCvwDr$ z5EX2O+6OcVuhPUt6zO<@3R zVY?}?g`7;R5TV{Cvyy|d`mJjMbl7wvCUWEYQ7s&=;VM|7OinY93 z2A#BycN;*xtg79O^a$fMVxD=O#A_s8M{CV^gTxyIdZ@mk?pBemTlw7=Bn4oWkO>X4 zlNA>9SP6-ptk5u^lpZbWY|S>_=8{7s4w87A#33Gv8b}A@Fq!+ZjU!xsl*C~YM@Ssy zmP>o|E!(SfyeCPVBt63N^&E`N`PiO?`2D@-N=hj%>eY(qWbxO%!-*cWetIyT?pU5a zv!Ebf=rhK@I2G1z6#OGREoC0+NqwwA4|Q!1>%As=%obV7Mkyui*JRXUy4OZw&`1TU ze(VY{bd=_pJF~I3aFlK>PFmW-1LFDwid&fPr5P0_qQ|RPr@uYYPuD6rL4f~cS zddTYB??Mz-#Em?en@DURv5~|kp3JuWw@`QMul|QxbT>XG@iDRN**Jef?1=i5+k8gi z6B3`2_>37OQ2x1k*+#}G5_msFdRnpeXe6aR1m*|=`HjpUGmU>Skl#uCM&e&2e&>!G z46H`Ytsw&wshu@_U}BY;#@{6V#`0X+{~g7;ce!byChm~9OQKLi(+>vrO6eV7K+OD1 zjq#kNq26pw%+$mzP0Z$cZ62FRY1YS&^?`P%KByZ}TWiwb3RoN#5AH!vTfYqMjNc|h zYJ`EdXEkwF)0bKkhIHiQB~4u7rc;G7l#?t#tO}w5!1}r>J(d@;qVfIm@CLAc8X%BUf)`qC!$*$B~DS|gtOT$ z+vyZLoq9LxY@WfL?RBEFeNM5*DfT+WJ|{*}VfY2=ZQUN;G7Z}5OD_M)DZX%uFP-8m zl-nfxl#H*P;%g_C*TEx_G1!?S1O~fq#Kb7j=QnQkFQ>Tb6u&vezZh!c$Kybs-j7d; zf{K{xLise8nBo#sU1FLG<-a^0%RD~A1*V?i%7Ni#ZnL6CRs=`Z8QBJ)CyxB8N@wFu zmw3~4-@L7N@qBDxcpF_}y-RFxiH!_z%BY6u@2ydSGOV+s;;=aUHR|z-PaB6^%KknC zAWD&~A>*)19Cqm-?9|cy=^5+7XeO+8%q$T0oJ*W@1-Jx+J?|3dT};?9OxQ~2GyTuf@nCeEk zKCU8{JkKRF++w<0Jnt4WxTM**tk~AZ95MZ09-A97Oa7} z`B|_G_U8+%igjBeyu^*3+!_C*<*X z&oS2L-Qs(Oafjfo>1ex$>o2##UE~Q(=Gl)d2!_@zoIB?RyKK1wAmvz zdc-D=*z7^m=%-sTpX}n2-5#;iBX)VjZY~-7^f;jX!_%X%PW61|QM~VZrgvM^y})&U z@QCvsals>gK;2T|zUX0Xeu*pm=n)q^;*v-Fs4DQ;2;>69{K+GJ^5~7MKF@ZJ`mv^Q zoh#q)h-)5k-6L*r&-NBqSlcb;WlYw%o0>S@h*uD(#qJ(R^f zFK-Rzd(mKlSIqN@`ChTWiw564r$8;_k|M9LykenO6mf|$k;SCZLB&(xthjdu5!dH4td34uQ(D!?R_$idaV|P<(R0)xXy8}c*iS_dBt(m zv4$5iQCAl}G$KgOQ;G(sx#|~Qamp)Bd&L*`f%}rj@a27D_{z)5;cIU2jaPi-6<>SB zH^BzL@7o}0&Ugjh&oF65PI{DMU;PfyiB+ zJUvXuHp9mbjs&aAu0(6elvkr+z*NJEUmf|?^WbEt4A*B3bk}w27~aM<1=yft;H34* z)W@;EGN&!A9b*jTGd$sA7r-zkMjmPo=Tkf}oLNK_jNnH#?5BA*oo1Dto|=Z5_A%XP zKBz0LInJ)B4(d>|&-7gwX5{m0AdCB+?->CsVJ~_JSM}Uh2T)qY$#U+bmEF`sNJ^_94=FAp6r242HbW)wP?#^rhbHBx`TB0i-?F2M( zHKPNMsUxa(5*_%!6`jgiNtl6>S-cfJH){bP=FhIpJKIsHHd>4nqr_-b+c|rWc_Gt? z1y$qVn2pPWg&2(kfOv&m2ooehXzaD*V`})iP$`j3{Do!UKT5zbFniXvIh_&?WE)ih zx*9t}MKz`sn)xwT)pgTKoLhlvT6N|=3Op9ieXan$EPH2Z`+PC~9-r{?^n{ymSp8%7 zO@4QvOlOZ&S#-ijGJLRscCJ8Kc@u7@NR+Yj9)5K$gH}^8E3jY5KH^|+dyHNMg%D3w z7;D0v#O}0sKKD=q4=^Ji&>yk(&x@nA))({Ap<}iAxjJ?j)loa>;R5r`uNl`X0IUvc zI_19&xExPfugq`VMOjYhEz8JN%Wf_!7}dMUGuI68nhTSU`j~F2pal+h)CoLHO-0C7 zq80N2c||E`TwIc7`2UO>$A zax0Tktq-j>SrJC2iNg&0s0MqYn$S5l18OtD$To3~Q439Li){98qiO4fO@Yqy3r!tI z7OhYe^v#{LPA_Z~&YK(awP;xX4}j)Xi~7+c*6boP{*gfbV{n)q!QR8JHAoCXt&2tD z2f@Sb2e6=H)Sg#Qx|RSQ!f`_c%J}@5&kRszD;ai&0G3eI$}x2v*yZA(&JXmpd;o;9 zNF39AUk7~iopo?gbx`itMLGJfH4XN+2G3|hrDu^)l?C(NKPNYD$!GMimHX1#_`Xc2_afAZae(ME z$}6wv5zF=RgY<#b_vP;XehkUaM=tt@*8Z29&^7Dtmj}^&Yv9sjW#NB|<8vwl>CYi5!Tz3KM#cwlD;P#5ARA*Q`D( z76ImOD-v-&t*`7<;ZYHmjtbb3hVe1i-Vh+GKW62x982@8i!1Z#TJgiL)*$^v4dY33 zse#QIVsV}}|FB+q?KnLAkG($2MkB`x*;B5#?i;O%23ZBG8hExu5pyho}T#e}Mp)(r*bKdtLXM~mydS%K(rtMmGX z`sp;I68Bu$Jf<1xrnFvKKNv-{p`kvrhS7wJnwlpxBNs&-HVj13W)!_z9lKc+^)gRt zMsF1TwV@OGYqt>qt3a+%G{XE$Gag4#(Z=?aXMMM^Vfob=aEWjkB>c3-9uR3|Zt9QH z1)DmSpHz zD`!hjeZCT!Gtum?fTseE)-9dU{K}S&<$tY)Jt{Z<9R3vzJ5n_7uyr6xH*f7&{?n?) zPpb4XnZIhr6)x3_yJJLyiaVB{l!2`$x5b9@nr2|bDXk+Y&9maRb-?cs^}B6bF5a)J z_h#EUfByEIHaH6|)^NsItnoT@IMUdriA|couRCxcyq$};Yk9^FP3+K&5>1q7N{Yac zOGAvEnn0Y|Q7e4MDuCR!qk-qmsyNA6YF*pW&10n-Rq)!eBn4ADreq}$Mvb!HrgIGg zXFV?>g2BAz!(mSw&*jRh^7@^2eD&#rVdKEJE2zOX753pA@??$V$!cUX;g zHw6+!eZ{Ma&-p5R#4TL&xWMv0h$5=8X!*N)jtbz>8dDojUv}Jz=dsk_sAqbR>?7tSd)8 zr6;X}M<1o9tkieD(&4m&-{We)0fMuRh+}aTzs)pmkhn(TI*A+Vh~f_te<%+KFlcqG zTY2;fpT}L*D_kIOeyp?BA8QMtxN)o!y62V z8G-LK@tsq1;H7Z{pS-j@N zO9YM8{KGo%3_kT?1{COPA6BMa#qWLSBcOlkWIoXE@X?bfKJrmjRQ>Ivui+`3lSQ<`+WyJYfRptp;8?vsZHxC;Kh39QR`h3+@Vn%*_O!^l z@L3<^=YAd!kK@Ci*TG50i=XGEL>V_+;sy@jT*eL4 z60sg7r>a4VpFg#fp0g&MPJkO?+3Dppvbf0?ZlVKLi!Vph*y8P9W)P6Q?&gT08*Xvk zEpE60;_6o&Qg!35Tm0n~cd=71m4QMJjt?h!M4?Aa^60y*{$HmsnWuTgG%R5*W4cF7 z_khfczFvfWtAEoyQMq7W_JBiQMi9f5P^_EgZ>h#ok67w~5?uaGI*4%Wo7VJ$rGMKU zk~`?z%Ao7qZy%BQjP;8BIlF zJ|9JsNyvCR%4os1rD%bS?PqI2rhhzJuKGjrWelF?xF_=c_Kiww4j%{J~eRSi9j z72icY2vYPFeR&T0iGCc%(H|u551jx*K+$dhaC(&0*FZ5qJSqkNp9|QK<`a5bK#bK3B<7P? zK;i|Za&YGGqV06GYg$}$p{iNL#}Hy6i6TCoU4Jf4M@Kk)mB9npJ;k4&o5dnL;6hw^ z#KxU~7KM{RH$EWo0qN_lc^4|uzpV8a5+H}iFH}nAQ(C(lEYJ?)H1YVqVAruYP2vmg zrtA-?ouK!>CGic3Z;3TqvK2PEt ziSwi%u%`U*9u-)fFE&fS!VsV$=6{lgYLhiFNfVPbJ;vH_(c}TbfBd{AX0Rh!KUjR{ z;uFLN))RhA)qxhm7qNh2&EADVYu%3%xCQj8(y`F4$jthwhBk?;em|)OA8O)+CO*)_ zhg@d;R5u(`@Tn#~(Zr`3FC9Onh94ykN&G?+UuZb#54miH1Lzq|e5;8wT&L${RR{Xz zye7_bo#!v-Ym=$?_T@2J_@6b5?M|`HDYiSYoIU-^GU%+>Uq7P3#g~8GK{VKU^|u^~ zDgNR&lftnKZFPw)F0mC_uDJ5=6A21+)wS99&AvVeL5_>BH^=YS*V`ed@{NIbpM8UK zKD;p$VC(%+D;h^Zn89r!#%u6=g2`TUgJ1O_*5p6NC163@>=ql{Vv}2Jb~7Jtaf>Zn z!8~J?z1awy(&;7xD!G|NqpednJ0YjipM$W{&iQj!1}GDZyF$}&1wNb`qo532(D1&* zFfaUWjl7lWdW*0~F1j_8rdxM!^{w_^X6bGpjj_>ZF@nph5zHMYtR0jGb=N^_=3nvj zmi5M88_~G??HTmG_08=Zte%m7SB-!cz%e9i0X}?OXLb6!Ry>DOVT&4!FatjKBFvWl z{fsu1te87pv}t4wyEBa;gfWp^h7T^6b=Kc^;#vnFq}!W7wrtAsJ`kHfU|TMrL&`DE z=qHlTIob2h+nJAe2j~@1e8}Xm%*-g+X&ZU1r|(8!S(|mYMf_9P6MIE6h{J7lM9HM+ zAG4(l`uuozB8@E?N@Hkb(U(-Y66}`X?v#TW)R>fig9S0TH$5mT6SbtV@^PXB4&Mkm zBM!%I7ueMkD1{8fC}-Z(XK4so8(* z(sEMA|94$Zc2Qq+`JIdMX`JlorX-{$xXHo^4WG|Hqat5R26*T;)%z;5G_(RUp@XA! zTWhAnxr3Nh^RrCM2K+mi5mdm8umz=$ltm%b$dA?uyrqP5W{>`wU!Y{o_m6&MY$5jPbq##Ezw%t@)OP0SPAHA;X4)+0GI zj7HIZc{+?bG(Znoz&$Gnpr)ze43(q2P=aveV18|c_tatYHAf)KPvijYzCP+hd*m)3 zRib_JtdE`!gJSh_beCQvAM;ZxN@w~h6T5_6ei}q$WKuYZYG9014#&df4KhLlf~iG2JLT$(LbuZam5kL*z)oe!!oQQY+Z;~i_t%oN6X`~3=1(-N;T}h z9N2sTRB+F8P->Ah7~D22l2%qnLC}K+BwC0TJa2Z(mT1|ETLwK&2W8zT>J9?Ti9%?0 zlq`v&&hb&OFb1*$VNX*8VzOYK;vNVbO-0hEK+EWmJWzq!w!=IDE|x_f6UeVv4ABz~ z0bgl7crOu_$BSezc8KLqmDubBEQ0KHPydFRMD|8x`DRIpBo*6bY=Zzmh9rDIS8cmmhoN=~&7JEBWFG+cEiA z9JOaws>RHTuz7$&Fk*m}8i7|GaD<>dII9QcS8;!rU zvoJ4#651g+D>%GB%&MPdh~3AmS0fNEToe}wIxo_UXf=RnTTu8)M-11Dg`up=YYFrk zOpL`9sY^x#{3Tefa|K8Ip`9sAHN6n)1UOIsh{D{n?{t?en@G(v5)p{*6z;$^A-};V zRbCFw=6E~=r1LC?A_n4J`D`K?pwhBLGBJ{~i4;o*N^T`m2>Aoio9qKVD$58GxmbqL zq2GYB9``KRlctjFv_}$-K9x+dl@0EZKu8UqjCX6Zr0PfHNI?(#?+eM@BR>~ZGp!<+ zMO{E}ptcP}hp3fh|7DPxdt^0(YEpviYfy|IGz_i}d*oykBGXr z!JE)WsfyI8%%}=Y#%PB8(V&VkD9uo%8KtFF5X(7JCMJVxlH~)*G=XNzW63nrc3QNN zUu~pRxj%)bY6}opm=hx(PNjMDg1nqcJ@7Eo=m9(|`*9(SIw4iN5;Zc8Rz%!KYlK^d z23$4mAxrJ^*wbkH7v&3;Xi*sKF8eM)k*rynE|r(O3Siz|KcHb{X77HHtd>r3v_!T} zrxsB!fp94H^Fqwt+*Hv1Ww|1qM$=MRHiOEeVp;~4iup1xgXYp3@@59exkOf}LdpJR ziP(hn7JYG)F<e6k8v3`4hr#X!VmDiu&(ZmmMuoH+)^Cu5NLOBJxs5~)|E zwe+IgU6o#ndxts9BSLbt^#?T8n|pz>&1@s9Q9b%wuC7KYnYTN_xyAUc@q z`R3s5j%bai!<-dw#9^p$xLq}0{#gy0>MxmEol+X0Z5rC*#-FH^2d(UY&QBMW18wot z&FS$*22OOU09KVeqbhhY0}<-;<)rGA90T*-=Q9OtGmps1Gir*OShlhu4STB7HT~yI z!)x9$5Uu|?ZZVjz$hT^cpri6^4XOyU*$yLP5BgCVmWkzdp`4wG5^Pyi#375hCAVi% zbCmp@aF1PhkqbYngt#OW zW}82AB+_h|T~oE}TN8!LZQfpXdf+U zkWKrD7M0wrMa?zlDxIf@xeB*HFs35eDTi8wEy2Qr8ydJtCigdn(Cy5j6wLG2IkX9^ zGp80(_!%cr#60c?BvfcRsi3jcBGNB@60N1!7#w1;LhAmQj)1RiD~>fNP>zU_G!r zK~`!&HGo);2DAfc`WsR$q;ebDXto2A?G&0L8!8T;hX*rrS6s{N3ZzOJQfp2>f>^0X zkPd0YgD$Doh+0t`@*~-uzYu8QVjjyFZpYy2P?4Mi3Zb91jp-SPS6UNr%VF873Dss` zwXww1My07ur~{{S;h2C5mtQskKQEDPoC(o#`AAc+%W}E0Db1#3vU)Bxq(yRAE{vn) zazQRN)e1Ywk8-JId|{^uUwP6v5YQnU>Dtsz2D*#zwZk1Gvq>~ZH>wLKQ#;8fCdHv# z_AzN#*!Oh;3xJd-OnQ`lkXg;>DSAb&YX%c|wfwmmW% No7OXt>lSGnzxR50|uW zPA>AS%7Vo0l|5R}H99NXwWN!*swBG=#!Y8SI=2R$Xq6n-hKlO^TrQ}%wBX${tj@gr z;5Jm?q7&pK1mbl*4tjyF!W7BIZ7H3K9|^RkxP? zc(@%(KaGY-#s*oDoMvZlv>&Iq^!;dT4fuXZ(W3UMX-0eG{t<&iBtAkal3nfWXY9x8 z_Tz;8xM4q%I-tq)xPbSkNVehh`Eu~?^oD<@NRHw3zY_TduHv1SI;frw*^et+IyD;M zo*cugf}|b*X~!3W=p8UV$fBA|fp{{A}WV&Sfb(E7-@l zWNtK$M-a}AFm_b_(=MsfMOApH3o2Z#U~DI`jl_1YFvl+0ryeE0bb;C_3#Ra3{^3Ym z8sg9NndfCpSL#eh ze5=Hk#CJK3J&7IjQY5c)`uogMNfdpMKABl6iS0T4N)|4gBiI%2Cvf_uEaN%xEH0E6 z$(4O5IsCm$V-g`k8&}7Xb+Qjt3df#(TJX|Ik#s(UEbQ@T2CtkH$sEplC(W1}bf^}| zVJa(=ou{_vv`8*}2nK19{E$mNQhw3EtrV#}OkEP}tH>*1iHMc(S-wi*RWe@Vz->0Z zAErM|@Mu62gYhf-m=W55h%sgVYE*2ncyiMX`Ejpo#->cQ)Q7ZtI`#HCU`1v=^f<>J`+5JYwvuS5@`rI zcnTkI;OoRlL&(8XQAooLg>VXeXpaRqZI4AHC z3Z$V9z&ZD{3e*8O=blz6?=!(U34oWN;Fa^4;GDoE8niF#Gr>8DC`bGc(t3f<-j3rs zu*!(=ncrpJr+>=$Ot8*9{S)pp!8*wR0LK{s_c$+#LDxD(cz_hi=8RZ)S)J_J1<7!%bvpDu zF4lbJR_Pju;oOb~^OYB1z`#yTv7WltuKY7cWY>YTn7)yh2U61k$7Alp3KRQF?0r~a zlI9`YFhMYeng#_7gB>L`k9Phqy~kbzawDojtR=X`cT02@<6;CPQt7?wJXV$ zL#R5o(jN|?40>1oIfRy!?yPWQ3p=ajL#Zg?&vI~ua%7V22|XNeKkyD~mFzN%9-~`w z`!M+KR?FUblt#sJVjfjQ=F&Xcjm%!dRpxWUX){taMo^k4#v<&g?x+CwR*Ze+Fds)| zL&V_m93iRSlH*3e6S7)vM`ghKY6Mk`zD4|Pk#L7P48s;B23H-P1_lw2W6QrIg<2O->j}OO52*F+iU_t6_3uH&g;Uk8*Eo8Rp>7>V&B_95 z0BjG@LlwL8X*d^;&8LTxY^43h6PP*mg%$>fcaTt3{yCpIYAjmBf+@|S#MJXPYh z(>Qrkt{P7%oP2LQ&G0Swz!6xzmdd^ps7Dw8dH6obf)C`r2^5#Ug^aDBk=TkLiUcs7 z!b|7SByI|e6v%8NeT%$1f%20u%)nX~{M<|o_V-x7*_)}amM=a5ro1f=Jb?*WEpZ0- zByXG2lq+~k$*?D}%hAyDyr-}Lu9h30q7IzA{S+NV^3c7gNN;kb&IMF4LIM3OcsXc`e5QbkF$tN4I5${b(!G$%5$%veCc)vgU9O*m znOiMSPNIkLs6LrG^u+SGP7`Z2u})*EzKIXSh&K^Ul>n>69{+kxtk)nxrR3b80iTVU z*r17xsL6r0n>0Qx*{p)EHUp6Sa5BY&<0J~vSz9%PXCdp_WYu}h6xI3oDb$gzymvY1 zMZBxpOo4-XmApKKL^izJC;8M?oK$Fi#Atn_(2DV~IpZ)s*4WdHgWQk#I2Z66PgU>- zOjYprPo)PdVnCO<<>f$2dq7t-aRmdCwWneCxJ3?_22yR2)2FHC>!wkMa2Q90PH`6@ zKTZI4PN&Y{FwkZ>#Z0G|#aaD03ntS-r?8x2A!qHGj@g76xWp+IJH-;t`hB_r8T~v! z!k}B_6mK}iDlQrQJley=+UyjYoMJO)z5hH_eE?=->1i^M-{A!EJDfZlFu@4-me_E_ zeI;CA!j&b|*u^z=sTwfKa5Kcox1w=%X*XYB0@yY)6b>V100)>*$DHCFr#QwXM`lpf zOc?wpoZ@|_IHACOz~DYm;9$Zzj1Qgc{6FawA3DWJZj>}rfonb!hgMMdGXWKb^F^ol z!6`0sg+FG346v22fa*?hg|jke!LC{@7tBIsY~Ko9;;vH^x=`}tEH&fq+0-H&TMZRy zgm@#A^qfuo&}PSMw0S4fSnd+bTw*zwM9fibs?MQG39Nu&JKEFwh6@y0YcMTs6jtbLm0w z#p$_dgPrB)F7cU5e9jeW&!f6188J`QTQCp(AjTPYpDyzCCsg=x9;LB_B4n~f@-{NA zxv=fK#`mib$$i~rYXZbUUFT3J)SoaPNWcL8%O!5P#9y4XalQin@q9(->I={ZEaDg4 z;sv*O(Txhz7oZKcw$d#YxrOAc{R`}FFD$UTYRbi!fC!6B~BxYj4v4K7YZuwk1EyurCWUIhD`Re zzzW!_oC{o=0))*LCII`NpWWh$Tl}ngU5G4ffpBvQF<*ah*3g9*3pPQwRmj(E&RVgM zVjjS@15sdiR1_GxE@Xqd5bl=*w%eSD1mlg!WDW)slRb>w6s|Ev)qp8i#+d5i$Zy1l zP2~_VfDJ98fmp5|FTyfcs_`xUXwyQEusmX+2h6vw=)OhbC69Q?gGJ&}5nX1s_-qk9 z%g=6->hN=xq@Db1v6zf@H_15X5$6IQeu^=0dF#A~4HzsU7d-YH;!c-+p$qup?iNH( z;fr%8wdmq5*Cmhsx7@UtD&0fz3ZwY5M_loUpBcrU7vG2C?;i0xqgZtbjbT)lEuolR zd((_5Uc1MsUV;Bl@v?_{8eb}!<^?mCF{XQ&I?sE>bgy{c%k-PUTbLPea3-)R>@{Wv zAk6ZLnO-pqb!7NUHlNmh$>!5V3~&+OQUagKK>fvDA-!TT*MI3HCGtC7qWPW;HDLtq zmF-`q{xPt4aDWwpGZSGuh4NtQ$LU+;p_eH&HCUR2($cRd8hS9B&+2wa-%@HqTV*?b z?2t2;QctAL+Nq>ha7eR5_I`yBeJgLhLN&r}*W$1gd~Iru%w9$v*(wS_^hby;<;-Qu znS5m#Jr(! z`O^xVn9Y~DD+%sq`RGb&i?a1Af!UFg%PVP;hSTxKU#Dc`E_fXW0Y!54>#)0b%cs^- z#n=*du;JE{3%e_rx(h-|{c0oLpcu3{wiYKQ>*ba=5QTNCCN^%7*cTy8TE?v-1k}s= z>!^yv1@oAvu16&v^Z+vJ=zO+g;*tLqfqON~6*3b2_=4zl+ zS~g@g_9T1c`>UZI*2}A_?LKvQ`gGN2g*6I9oiz%?j5XM-l*magz6c9rLEO|4+x9!|Xn09o6FJs&!PKpWlHNwJy|xK^z8j@i9U+e$);G z4|Zbe=G(R4z0^S!w+PPzSNO3hnIoILNe_mds0GhIbR5zv-=w|~`)Z)-*GXX9+C~|3 zfh+?f5CqR$kIMD&m40!GQs3iiOVt0XFT_emTM?_yc|%vWl+-jp48N+28I{ zox$^(t`#`oNon9TqZm{QDVynT+;3TK97;EPvKl8Hi$!Tco|$(RJgjt{^v3_i_>Q?q_YzpUq9zUz3A3K^>}E`{;xmxtXp+ z22Y^XA*4%*%9nEF7O0`4a@rPzIBk?ETVca(mCtRZY9W^*!GIilv1Kb}^F{f=RvL?= z7PA=6o_9-n7E>MU5fM~n-b}<8-*Xz3%x&`JZ8WL0BYe)11%&TmeJQiHBb4E&EZ9yl zk6=wv+uXKhD$aNDC5t?`_uFHsG5J%QPSGKcBN}icvlGHYz1+w$6Wq;JWb9qcnH>AQnEY4uN0O9PzZz-LhnO*r@f z)L+)&Fr1h;!o)fB(}b8e;i&F#m^4P^Ai#I3CNJ!yW(CvGCSB{#-vf21;<{m(>e*#!xx6xqTpeb9-b98mmgs0i-S2fifqm85%>wg*4OA zMxk&D*aCoDg>RrVyw^9(tC(mD~2<6!1HFVGpI@tjxEUswbZT?!e%C@(m2YHs5#TC6j&*0pC2@ zQ?d{0#hoF;!Ba*0c{1@i>Oz-_K_~r!T)CGT(;azcFYKRF@~^#!RG6&E+Axwg30NOIL`~xmhT&waH60%p zxreo;|1RSWE3A7ThL~NE;}6rzz_#oWYLI*lLsf1B9gN@>h(E$2$(e$ql<|IAK7IsY zDL2TMi0L%JZs@|H|7o-IExGy#jdz{U^z9|$C^;$ndCUW*O@%CJrmHQ0V8X|m&N1P{ zk_2WHxW40P9S&A9U3mt{FOE`te=V0wAsfj~e0B;CSL<-lkHrq{ZRyj@0*t$5xaN2G z94sNO;mnM_2#0wR;;Q4K+NUhGVS#j^=Bo*8fG(u0^*fZ>hNaARgFr`{hs`yi`c5s` zsd&sJe%I8ncWEZ{fN+`)a{=iW3EpbFl9};P;bBBO$6T{iQt}p)Cx0K z6rc;Ph6&FBXguL!xWs3nEcmJ|gxFUFbDn~;(c#G&RtC%%q9n|d?*jwC+z8}_X6kt; zBG#FwnfP%IkZ32~air4Ejx!f!NC*(Z{f{}H^n|J!`WqGH^M9P4q$=*puo5~t3yoL zILzDKzyEq7Z%nLNIBD|KCs`$HCf-6u7#g5K0n39&Df%JsA1^Wt3jC_(`(EQfTOh#D z8Hr>kqXFcw1O@ok#-=sb5l+@YYToi9d?lIh;f$*MA~kduvVEcW0WlWKN$*p6vEZ;H zFOwYRr8=Mxytn!ijU%QV`dn!B-ug>&+xs*T=1{E@WERY^>7y1Y#m3-ZFc&XC7@2N? zq&CGMUrKx#6TFsYGV62a%Qd?sKwwmN21-^0N^F5)LFI4DaGRAHK0~hFUe%z7gwyu~ zxgdIgpRAdV)(Q;fUR{IQs*ko>W>=1~O- zEiS-|rpg#K-~?e~g{1MY&>f(%L_#nO=oxUxSX2fa#t1%tC@IJYB+#6QZ(0afyl;H~ zH)jAh=l>ly9s#2uoFEXm0L%p)1muwkJ%8IfW-Px?z`q{A6hYa9v160zK77H+|BkN{ zq;UfPFlM0lq04h;J{LfDftSKr0jvlKXaI9@NM18XT_=mmg3?#cnNbiTG=3@M>)~L! zd;e3joD5Du*q+-Y!-EwEw8UiPVftH!yP#QIEab@^Q_Ig&Vv`Jg#GMp|qkslnb~cR2KO3 zzCbg(Z76JQzyaz`tc6@5gb@P}g(iAY9 zF;Gx44-7+j?UP;c$>Dh*0b+pTlL0R;IZU4d=`3J;5Kjcviggn2uJ-ZVhl;vK&nOEY zZj@p6D#+twbF=AK?7les4uj`G3y^fUZ~||Bhrsyt$yzcyX@$$cf2y=?xRZgQ5V}|) ziOL%IqyUT}LKT%<0fqsy2-gJL+I9vf57GcifzNm$aIwZ=Ljo9k(Sx^rys9U{0{Q|s zIC#3bAlaS*HjKc%Zf02Ys504_DFCII8i86&N&sO-2iT6`9#GQ728@eQL__sN_dXF0 zrYU21nal72`Qd29RKet;4knF_9p(=x69^)&wjN(JmQqC`ViG~k4HxqH6A0{nU4C(b z@?dPV_<*V>uF_0LCna|Q&c#Z0&-9n`KcL|-2><#3r-rL!{D-&}bz08-kZ!ByHhy;g4t?t&!TtuyAk5b|1s0T_ewZj2+rt8T$zhqqQYdK0(kXt&@L$iY4t$ z+4wUW4@Xn+XY^>&@+{$x$0nQq7ir$bpEvky8;`AI?ay&pVS}9XIiQ!wJ}xt9l|>?|_5rftQ%LK6Z^ZHY)h^Ph^=ds9Nkb{JRgneA`eY4eSVR;mzMI+3gGL zU~iRd_=5Uq+JbjWLca#}B4Hw;7FJNqH;iW!SJPL^M&D3O+-giKr!jG`R8dHn$1u~U zzad9{LzQEdL_~7~MLId< z0(J}Q<-rTowGl{G4pvVxzQGTT$GT5_aUTKjSumG*Xyt^jGgfB&69;YB!bgpAbs%<5 zeZB1b1J!0u`T?HD_43Cbs3V9W!dNMUVXmUasYyrim=LMM| z3u>y|a2TusF5yr82e{-PH1z(2NaVL=yPx3lxF{F?gzerZ^2ATz%#HHGPhi*2Wwp!j z(|#_8U#9kDw`#r$4p72@Nre#xo_gmprDGd<^)i}#B15jw$9Q~o1suLZhW<=BbV=s^ zjQev7&f;HoNru)k7oU|ge#U<7l6>Q5bZ}K(`I%-0%CS-7@=3p7KXFN}_=P%{J% z3b*B7zd%?n$%?;HqYAgr6v7DS3pZEs#&KP!az&2%m4;}Gzn7TP|MsFPs!!mDm488K{-?JB`vA3^3%y!tQO^?-Z|c(G9kbdC53xxGj(W zPE~w%=cWUl%R9egLw-$WUZbekYYHiDUWfrRw7g_sSa?=Ga*fif9ynLXRwiKB zrlVOwUG04&@m9D(ZE)*qhvnvLRG|Vl;91PkJ}rHF{ha*z8r6(gfgH7nFu29%WCAuy zNw0G?*O+i+6l%Gpn5YxMHRt3*f8u7rnClc7`IeUKH49pWV@(h4(+uKF-lAE4xt55 z6mTN2TK2Wtqf^44GzhFqNE*SAzlJ)P6kx*#&FV8*hGRU=o@9=^9T2 zT#SKqjCTbvo0MJF<_unou~I6IXmgViLQX2U zQ_so~H>qVjGmYIJSLdMvv&0CbI^GpoZU18i8XLB3B{LMQB|SEYH2 zx>T_T?`@^l3pfeEHN0K0$8!l#%!wl8i80tS%RRSfch$w;vr2%Y7(Nr`7fcD}B|JcY zD|Q1nH@G5K{6#Bu)q!okFk+YF1Ggc~m*nHOsaRLg3>-t-TyRBZ{f%>(E3)n1wE7E?k9fQ9je!OGp3?0P=J}A0a|eauSkaEVaty+690)$K)h||vuxo+X>0 z|3SYby6{DtPh@@4(pbgyCoL5Om`2*+|B2Xxn#QCXui>AaL)|J)Z1t|l_D=0XPA0gt zWF(uqw1fXtzh1KH1VRgQFP563D#glCMfG&x|zf`dRa*4yXYT5^Ct zJc>WC=l8?9gD(u@R+D+(bYGI09&I<{Q5dQvga6OK*Q4Zqt_SG<%=Kqv_Yf`jAH!nT{Qokn{UKUY ztTuN-w8H-~y0xL&Q)O(4V|HT%WmcG0yPD1WS}A8ScVJt@3TQ%pvcu*d?AbBQOL9S& zwzay=Zh>_mAQapR`y-)YFK;)&_KjIij`C^6wUoMpB@dsAAl&-kw9glGzhKdaKV&C7 zC2C@Gu}*^9dib^E$UQLCS-)zK6}wp9DQEk&Ebr&=Fv9OI-}Y;KEj%n-d!*uCHcp{< zfg3D75W939@#Qr+HC(Hk5zv+pH!ibvovLcn22*FiV+k!J&xdO>|G|n+meJb%V^a74 z5W2|u@4Oaj>!K@V)TCT3uf@ui5t=d{Hb(ppzB?769iqMRWnF8Fc*P64mYi-YJTNpH z(SCSGz|Pu#WaqM4I_6zr(S+n}$W!Iw~E%_uEWK3ra_@(*hAX_-A#^vK`>nq4XCOLBAhAT z{|7?89Qh9x$4IWqcm59+C&l7?vIL2M3@a9&9HniwR}gza_%{Z}svOX%9$Tl% zeigKsO$laH5``sNjIUPhvTalCu6k@Ay>~GaHeXwB{eNhOEphp#enDDM(k@O zl$VnGIg5lr&Rh%!k_OLzj>>{GU@~!f#U=Q&ru1_Ynk zJrGa_4&3>HaG^c-f=xJH9R@ZS?2tEw-4%MqsJI53^7wQTi#EoD^}lSG!IIh+l G?f5^0rs@R% delta 27018 zcmcJ%2Yi*q@;83wIW5Uac@om=J|Q6?2_&@8B@exYj!3!E1R;R*VogA5K-vQ=AShT6 zr3C_nrl252x>pn{C}1y$h$txk@9a4zp!fdX_y4}1&&&1ZoZX$Bot>SXot>FI%T@GZ9qV=?;jNpu;Z(3>!9%zS~0Dp#I{2VvXR|xvsvFz7sKOl1P42v z0S<>P)Z+Z*cM`Kwx@Mnuj&2!4;eS^kjF`wyM?$l&q)M?d1N+M`7c88v?JxZz_a40!~w0|$@jKl~BE?z9RV zF)kj*R)MdHw9ERJBcXV=7N~%_51cf_R;~rBLboB~CyX99#I{`vQe|@_NB|3iAA0nW z76V6)>|ZpzXt-^k7WiBVSW7mOJi&LUM4PHzqR;6feL=Id+1m5k8tp|b=&Mb$nf(Da zeW#|+&^%|{G`YB{%^*`4nsw9BJuub?5y2uv-(>Z0b}4?Aj96h8vH4oCzM70Ue2>f5 z0`z@k#N&H>zUDB=NDvA7Dl%CaI-nvzAb{yGVJrWR?Wn7ScEiV#JH z;jKwEBaNyeRa7l9(u5(>^uNeR_cm1%)kJy~jO#6Ch>T1v*vK?(^7T|owtBcC>6kU# z^`LVr#p|=I6RyN!t-xO3g)R^UnVQWo%}}GcFhz5HI~grNS4+{tXeC-2twk%*x{cAs zEH>JTHlpo#qaA2%FWQOrV~q}?L#q%U$sI*UMpWoU+eviF)Eq`X_<8AK)HuMGa`W6}eL_gzSqL28O?lB$& z+=KUk^)~~I0iwScP-G1Bb{r%I@$iGiKrvXKPQf;h&4=3OU6)O8j2CU zy^0^k#D|H8#V{~4n0!5kqq0a07e$pE9wA0#YPvBJl#R^Se4R%D>=7|aJd&^Js%Nk< zT8#EC_82in$2@qhW5rlrZ!S2DabjHMl8+bTtLthBZN>y(o{+C4Dm;nCM2OrZR81-} zCX2~wHZjo}9n_Gjl)oC(okD_*#%7SwL^KhN^)Ic!;I$NNZ3s4~k99J*iQ|f$T3A!l zQ?1;Pa++>k3TaL6SXrU%!xnhw7i`oM^}rG9>CoEu1snH?`@olY-vpY8W;{{Ii2ka^ zBnKO&F!9}kg=r3onim-@M2j?An5PlBFibkVYCRM-jP_e6F~B10UwQ`q&d>)@sP(m; zTVp+8IJ>9^u9+{?HS$GmkuU7}Of4P=>!YQ9kcAkXDtkJmQx zM2^U-9JUr(Y84r^MQx*wsDojRDp}gIcI)SAiPpld0hXxeuzrjBH|f^#=-w&1QBycX zO`m``cu8~3m65=iEAsU6@)j|>GzzzF$2F|+8X5Nk_I@7qM6A(EbQisZ!#CLn(DFc$ z(OdL3`iMRlbx?ek<7 zYc~d~=;T!tKDd00SKnNahsDbm^+f}wt|1nvAuo`^)Cdrb8KQ}3BpQn*`d%obVb<7` zArxtSkTORUcS zf~IA#V8d;?i~w_Sj1kBj6M;OYw zgsyKTBV2^@#*GjW`a$v%=kOC}Ra6b{w8uY047$bggyX>bSP^%3hQqWnphSvWQ#13tyd100~9rQIR8pj z&NY|&1o#9r%G#8gSnY#aSim}>uBdmHD(@1`yt{-ut)Eg89e>%WiTr#Wr52lZ!zrBl ze`oTMwEx#kw#ur;{y*Su{r^kuT65D3dd%9Krnp&O)MLTF%gqK@j)o?<*+?`H4Mih; zr*$>Wq&KbF=@Tf{dL{iV9k3p)*4TBax)EV+xAs&^Ma8Gp9-+Zj$BaB0Vm+DBNH5KR z+S^{$NH*)kBzQjE8n7?Xx|ER#py15>jKN-MsO4SY+M<@It+OJngI!Rk$fzsovS!|A z4bSY<>gR~c1;XA8Qko-(cPE6S3HE}^2sQx|!n*-B4WtJ%2nC{0>~ee!6JdIsbvv_a ztJ6^s_y|!&MDi|=QkbGDF+~GYj0u=nrF3EyCN_s0Yz_(74)G!$m>#NLwbg|vNI4Wb zBpsN9!Xzp&8Nifk0;VeKb5T`c(u_13B& zQw;53s!mdeZ8?O9ukAaLw=pp#25k$L&Xp= z)UR`z7|L8SpUE?Zv&|%iGw+L_^@}R`H3EZ-WQb8>gcvDCK~cBQd5}g~ujV8LgU%KP=SCNZ7F48jSOTO*z;=a861Vm6661o+-H#skgC8r360 zjpbynk2hA3SWaRE;p7jfDJaaUUbAfnpUP}vtYf456=LSBC$WyiD%BBwi!2fy720a$ijzGA}nR5BhU2iQOdjkl2eR|HAF#uCEjC`!`7JBLRE< z4Z_}^o;wMa%&pvJxIs0}OQprugL&yOiwIiZE|R>)1iC8KUuLb$O8~^qykyu;9fQ)X zKk}C7$7&l@0O8+xN3G{-JxiR z7wWwOo-Ak>Md{Xo{A|jw&NduQSzg#|1)F1yZWK#3tWh0etu>9(tPAxoQ}uf~W~z=^ zs$)%W$6VDhPj#&2>sUyIR(Q))O0&Wni_{DsiD8CYgff$r8L11MPiP#cdWQ8xvsi0H z<3ehSZi#LO6jdNbg)J?-Uwf3UjUart#Lu*2Ac_x3aEcY(wjlI!&xrZK{Wc8cy@$To^b`;ev!e(Ix>z zEpIbK4U}lbx1CA%m9K5Pn^4iWeSa#j_O_pnzXcs~$i%|T`d{*=iQ-Qa#h-^e{;zpi zSHad*u<3;(NLY&sUxBpo-&E`KPD7}bcM7f56x#3<$}2h#An=U3^|8ivolhO{Z5q|I zrgwWCwavRr>a6-C)n}ttuu1Ec6J@9=8_lDeR(OwiEL~2I*!adcHQD~E0;!7d1H(wv zGs++AQB2gW{Ii}_DCJdBIt}FY6@j8JTjKj`<1X1t^n;8Ywe((bxUppQsuR~u1ZHX- zq0-*3WekHH`BmCcYf>*$|FD)Z9+eZsI5A#KK*uA!IyUXk;>Y7RBSGflC+Dz7NsDA2!qG%uD#pFd{ zfyJaJS${oHosL?Wy$4cPtF*U~8EU*pEE6x0c#*_Q=&czqlX#iH4>dNl+&a?3tbg}j znBv1(K_-;OF4j{}U$8%Su^z*OruAuAZ*y(qEp9nT;!P57kvPaxQ4{HC93pdfZR2fj zKTP5fiML4{=AO6uJQ&`!a=vFsoWXppqP|0M=R4cC1b@5rTT4mh*ZZ|5I$GZN!4RVE zR=fTQblV!zzZ81$YX7mpOVVHyM~MWrETab8Pd%(d1G;s9jb95R*2aB}t(!{5enLha z=6hW<`b}Ao8XTagMQgsfy*92Sw#pmHQETA9f$=?#KH*9ck;P4ggQRy61b;!%?zUZPa(u}U6lju6a=q5UdZhDG;sP1Mm4%{9(;Ce#J zdcpx%Y8eK1mA(Hl;Uz8LA5L3gQp*nIDw zQW!8enO?Rs2B$&<+7C{shruR55<%2NSVEJ;Br$OWyaQv!WIe?<$0;W6RF7hi$HWxz zsCW$L!^*)`hNE6U%TC6-B;KVE@A`x0 zf0GIJyvKdck@z=>_eh*$0r3s@zWM_9(FY{({R7fd$_G9iNohSH9DZK?Oy-qb;~FFR zg~ZP!u95hK2VOBOhniZ4hb6abY5YOr51$afN5(A@w}_o$w@KV4J=^$`#Gg2>D+&8c z$@Cq@S)z%*NZcV&q5)@(;k~MM^GPNqFh}DFlxl#RtBE<9DAmMVhI?iB97?fj74?DI zm{-)D;4!&4A{v_Jw-G&Qf>k)OGybj~Su+Sszo?0en!d<7H?ok6Uu)uPF6NBNi+ZcJ z@gpPuNfSS4;zv#V1mxvoNA)0dKm15CJ!yUU$N-vTwHa+tb8GnM*|ANGZFaHE9-=A! ztRbV^F3RnC9V>8*h%t={yQr|k!3LQ{+b+Af-weRUblwzAaFHHvZ$RcE$#W*xC9hD^~<4)KFS{OAxrF-5Z{ z&j(*)rnHIzU!QiOeY#UjbBd>(V!9LUW2Yo>%Pel0?G!VeVwO|P=9U+y?p67UXwv=nZiA0N%5I#$YK0ta}(W67|g`r~hB>#4`GF{#(^ zy_t3Fv35`bRUXd)YYQHaVF5hi6i1v8z=4lX2|65YoNoi2PVv5TgzoOOy1oO+5?avrBAoi82?uPAP89a@#ic5S6*vh^Am5a6f*9`EDOMK-LU%SLN z3V@x&*cagDw=VImOV79VPVF3ZrIzt41K)6o>n`!DOWfd*Q>JCJZ2!S6w_M_Pm-xda zZgEThX)J5cPAjA?);H4{;@adrALhIHrm(<`4h!94zFRDCi-m4=vK6#i#xbpzkw3Yc9A2zF%P0oSxaYa#6ol z1AfE(zjceR-QpX!_?BsFKP!=`{()P5bc^rZ;s>|*ky{?0#kz0VEava!Sq*djwEyL1 zL-7uGCfphh!RX%4dUv--St>1TW)T&!L3fHg~N>|m5Ky+dlw1|g&Hp7`2 zMSvW^!3i;fMNl=2T2|3;iIYAkn37^sA8`8?Z}!UO7_er64Iu+rvtOoJ$;0H0vr4IJ-2DH3oi8yo~mh5tRn zS~7n!lt}P`mOQ0~0QdXCj#>j2w8S0YLIDi=!#qTDEu) z#{GTqlf`h6d2g9sw=ve+XPju3Ww{p~hR!A@VB&Tg!53=$!95f0xm`Z;`URoF2V ziMA+qsfj3VgKASaquJG@9LYXsS{53y9aUqT2@ex{=@Kwa_9mmvD|{SV+;62UiKiE> zMoTg=&%sLybX-4b0NU>ZgRm{B72nl|tRAa7Zi)qMpqb;YLt0oUaxCB!#3Z1 z67xtrLt;Mc$nvjc0O`NiMI?yDPzVkM9bLR47lF{c6>alE5v@Ud#2c-_eW?~yOf8?5 zOf+hn2#wT1&$)+Kf*uU!!2pzSSt!h%Qn|F{bR&sye94vl{fEwmI=|)ZT%;mt4$OW(5 zs~Z>e^0wADadT5naG#^Jau$u?46mF;WAoR#MiU@uDi9MAO@UaPZMWh5Q3nQzqn zr-WnMsJ2A@Xv>?K_jEGmmCU#M=jy_xoCu}FHUjS>1uU2sf0GF7_;cszerxUXuO>Xe zi*r1T-KzejnqEbDSNB^(*7T;s*8Vj;f_pQjVEEr6^&?iw+WTm`_2AkeG{-u$_Gma9 zdGQ?P(ylv!j{7uDh6&VYZr+#0*C6ZNwWtc#=vt#j+f z(QK>jD-&pY`RlLLB>h-TV~V-lz`YOh@R<3Fb!+`GQ1bSxrSxWbm)8~$^|vl=Xyhu( z!ggP7iH)=9q4M<`TM$AH-*1{kL#@G^pM-1a^UY5q$}nWhB=?&+MmYiWi!H-IdWW(? zI#9l%ESl(Ht88my{k?Rf8V{IZ9@UU^U|F}e4n@Afr{12l~^&uPXeG~FogKo42Xw>PfxVs!(T z3$#HkoY&Z=Vp$8f4?yeB+Y77A%rTa#)@5*uXolq0t~+|5b={7_D(}{Sz|ppvvObDRIh6WZmO15Z8sD4 z`0kGQdsO|6+Eak<_wV7F7uDaZd-B^Nh+MA0=~u3?cpr!~wrgUGCh*tkizM&h<{es* zu~QQ}HKRfk6`I;%5Xe;l#x70l()0t?BYW2Yan!y>u2-@VRa$QK+}GW;Ak)ag*UkH? zVrgr=QN_BlZ$5|yRQN}k3}qnpv>4%b^STGYr?#%IGE|3;6) zHcl9HscG)kpl7#P&+Tsp+52pN549KCT8|&73n?r+aDWi19{bjVG}1cr)@C@>iw~|v z5ZXA@Fc>Zi{~@`<8hYqqdc-<)C_Wf>jml7wb^Xwr8IKtCu`}xDYbOG+e|f`v9q3g! z9M<()8hfoz-tLt)5{FcfXu+^Pz?Rr@t=Qi6yMOjty$&bS4r|ikG$-8oh)h3!crpl! zIZ~bWTIP`^`p#S!Uqd<2!Tx>#JaeQ6ljXOmc33|gc>oh?eY9rK(paOIeSz4lPaPc* zF`6BGLGbS>YV96$zIAi~u+Kd+#iR&bOC2>Q=KYkR|gq6JIa^f1JG^PL!_iTImyw z+nTstiSj_8@uw#K)bvTlUvU1YdVN@V;J;TAwAf4U)r0@>qxY)QOv`aDgUZWu&Upyr zH+X*n$lvt-6f{@+ARD0FKKKOw*iwgiGuD{v5csdu0j3t5zYofx`1~?jX+?kd81O9m z5O}QJAGU+?w|_K&mRnOknu@=FeAIy!TCG3s1DLfRC%~`y`p5NjmHVZ{g^1-;mndb(Df|xEEHYl4{63KmssV}_b>B1Kj@c zQa_qvb-0`yQ=trB%;cty?1(_vC7c>jVU=92YGCBb+y^g&*Dy)IagM8oF0DhC`v6bM zm4x6^QLy1)bs%oL!)kpcGx)Q6;yGCIR5>cq$8-#o|4F3>Y;~?^(%CUw3YA6%=ut1DfJd7!g{wfLE@|mxax*+k- zhwKr6jb>#2n-h?Y1){NR1AE6CXYLL%#&e{DgTFrIishPsfXhTNK}^)QT7P`C%#RyS`4{FK`!NJhgd>l zDaU?8zKPc{5MsO1AKu+jUjLg?stLZmL*gB!rjA3sW@_K-#t9N9NQYzaq^kKuH%^f_ zMfy7Hr*D(!M=RvJMC{J2@2aJ8VAwl0j&hrE9_Mx~<3n~^i}NHtQ^R#$gy#oQp1y<)5sK~fT;v%#av9#d&@{Ao>`)Wj)GoaUw*Kh+Pxs=TL( ze{14B4LYLH)wGZU#5r~!YT`o;nFS-Rnjye>K@*>8;sV3$_QF89T-L;8hWYmD1bU); zz|Ui~kY8&WJM3b+UF@*q*!%34=b*-(yndDjlz0AhC(!`Q^;f9a%w5x8{fyHs= zb`%uMm$%0!;!G=Zip@^3#VN|1EQwp4VyhD(ZGLP`{Idx((6&FhW5Qo4RAe>&s}pKU z{~Cf5`08J~tAi2#G%$1xQ5!3SJEI{KK5ckzVtL_zvfjOu=0LP;nDxh1fkupsP-=Xff8u9M2_`lDv`U0X45;;)F_{Z$tfCThe4(h z?`B=VLF<>~HjU~eaEcf1y#A~=5LKD=w#-hC(^K+EJ9VLAdD>1h9s-IW7Ho&%fzRe8 z!qnU%IA4oo9GUP^Xu!?sZ9cS_-n%B-Lg9Sf#2pj!i16u`2%Zf(avok4cJlN6=a}5( zp!&35UUg8*gz>m$yG1H^#DF@ob*k#`upO-rlbxOP6pfUpoHQ0wEO1dqHCQ(OOE0#7 zcVfzG!u!vE<=rdi2T-hh*+n(b{cHdwaNHn!M*YaH+2UIW&qVr_}`4%{J#$QdjJ*w9}k%*9YNF_*P&*He77&5ksXP@%qiL7CPp6I;Xs%9i0s|p~){mtw5{BxrC7Umh zXejbQ;~|~;&<>drPSvPFwhpJqf}l8qIp<6-mG6X88d`q}r(AkdrbN&X8X;#ykl@8n z;}kHYz3-4)BPfz!b$+#-i7Ci=4q17~88c{S(j*FxmaO3$%no5JX>IE8A zaVUzisRndVI%7l*8D?J%Cs#F44zni~S6LTsvd}8kS*(zFxkDz#(7+n-p!pO1(4_&o zH1Ky(?oBpo8w+InAqQ-Sd@Y8iAlMh)GG5cwD!-ix2B{@f;Va*UM$kK&Q?O!04DVWa zZ1fW{Ck{^qc!wgCkb`>|QiB+|{|dBM4vV9q5UA5}w6+Es{7yKK)l#%n=Cmq8xtL$Lb%1r6Diao2ZYt(v;$;?V^E}1g0Wr< z^)T0bcA5I+VXs6s5DVd4q55AIG>rDjLIb-aR<1OtZ~IYDyx4ugywmth3E)zq;bjgo z#{A6L2{IKNR4)6rSmlNy<#|!O5v_!!R5nYcL<*DrQt3qsTUM32R1bxd1!s4GN;iaG z6KVQN3e*tI&0nG*BJ8CtmycG3Mv9fV@yGFb6TnO4O}RQKFIPncvk5s`0an-UQ8G1+ z(i38l_-hxqhp1;8!G_C3ZZ$k^ZhcS1pfn1gU|%LGJDv~7N$DgC4*0UC5fRW2C{LW4 z6GsM6gcDH}tMW$xHaBnW1YW?yb-kW4`F=X}3%)0<9Ozq|K!*qzhxX#Wnu;;#bP(6DM3nO8CLXgM(H%!6|K-| zqcbR)o|ZE+AQ*{qcLq(O88R=E<|uDQzPy@Ad$dwgiDUB3>a>XF%I;az6CbZ;QCEE2 z@_rO%Qzw*GWm6O5tt4cZv_UFopwE5N0XwQg5qlrKK1ca`HZAkO#&TjhxV>qzERCXN zSq`18xrp@#*6XDM8hpJh(^%?g=%HxuCJgp!5hR{Ni&%0?4Qd&+1l&NEU_O}HW1I#~ zFO>l`X-pJf1XWYM$mgc|$Y8eQGc|FL%#rWbq-W@PIUpAdv*hAjN)29_jH}86;z7JV zm?;nB;w;-HFXmEG5a=2z1|v1JRJ!x16_>{%GBXzC`}4>^|0#L&D$SFrwP+1`fxX)k&n$p2qq5fB4si8TX_#ZBa`Y;3z{zn)}zMy9yYu%j&6PfeP+&*8|&dz znlI0D^JkqHAH z1~jA=S{1CP&POB5UAVFlOXbeS5EDz@YK%kIk}aFi7D&tWCOB^`X*7kjTu#DS)C`dz zUarnfm9&g*O0g^*9gtqt0n)LkDHU+JC+O&j^2be~*sO}1O|kQM)Cm8mRg?)-Dvf5; z0RxO`MxF8TdNbOIQ705o9hBA=ct>rIG25$A-!D+3-oOWs(oJ;6?Y&f{nAC>L-uGms za*PQfvMQFC)SBv}K9YU;OEA|c5ykr=8d4X{TP+4#Ee2Z+&CAh@UB=B2RBW5@7O=%< z%4b?YT;7nITTopdqAt#lx)}2N7Sxf;1@J%=pxnGA#252uNxf)=e7hwCV}%TCMRRGn zT-u5n(?WT+6|AHc@@6Y)<~o3bM39xYwnoH(!Z1%2(m3JJCTyA7p+fmYYs$E1_D0FxhAX!)upWS96Sb`%8o8SL#F8~(YnHX4bY`>MtAG|1|yC}@fx&ZUh z7~Bu|2~4RR=B-}D)xX3d7{#HeQn|-leaZU~+*S3h=lyul`!TC4x=f4r`F~1f8J90c zz`yeVJUpfHLoWZA3{mTcr;DXh>!y%oTB{9fC<+S=z z`D8bs`77EN(=V0lxcpl*v@8PpXg|&6m2p1*OsTx-9meRcMr+?4yRuYH?oN65SnvJ# z(EAb8Lsd5RevIrvX(8Vxv%kfcOD|V*)#YeoHHlRuR>RROPjS^J$@jRZK}=v+M!f4DpQN z3_8^UPg78xqN<}kCU`1P7OEWOF~L&jcUA&Lv@hH1V3_6 z&Qaw+kNJtb*c-IWS=I-HeJ}I+P@%CTNxc$jSozSf5qdN#;uj)#1lL60FQ4l}4`M<7 z>_b(9uGOmC6Ip$+NA~C9p3Ez@Lalw})JF0x%bRjjD*uJ9L7(MTZqM0VK9O6wJ+22iyST=-}B-^G;55nKfa0UpN8R#X<5^Xe%N|&-`?XX$2Ew8(mGuV#_@r{K`Zs&gK=@B)%Dn^eeq_IVe<1yC zLNMK!u3Jqv!(&1)aSadws$323&|C`9 zq$v!oVX8I7V?vsAlo1ApoFscpNK-h<;i{bEF(FM6DC2sE_C&<#*&kx(`yI;I=8&IA zlp|Fc+Z^%}g)&kd&>rV8AwSV5N2_wIr`Uu5#h@ZaRm6BWf8O_OA040&AV9vS`zS*p zK!EP*6(|G<&|SS!#bZK%5`iyK;fwH?5Fp>19`q0Qm=K_3v?DnIWxd$ry~g`BP?*R3 zH1{426zVY{CU-SZh{uGOqyhmPY(Nm~F(D>ZQLd`WFk~SnX(;1K9NM9pAS3u)0FkcB zP)!h!YA9Dz<;Vb!3GwiqmFVC`SzdgIQoG zsTr-8*N0LKV^bnn&pBKE2jPnGoXC{`9wVhmHh-Ara0=GlvjGf1+SOeF1p|<3byq+! z7SgNk3Ml4}l&ZS|iuogp3ffM16m2f7_`S3`v7+(N#C8$lV~l1_mmP;eqBqNt!$9@T z1V~&JT+IDcD|sv8o0z(W?U#Fo(Q^7wb{|g7ir#O1x`$Di%)g`V z861?cfSRp34Q$>~Wo--x?sLt&Y(q}{Wj>>g9f zIz`mf_&gC}AB($|e^yH9i+CL%-$_`DMMdwFtXvy&(r)<2}ZQjJeTI5Nif_6=FV9EMA*VJf3AXQ zL?F$<`mSL$88`}#;x}b|*O)9OO*E#6Df%@za2zb# zHFEMenvX87@z@`mWd3+u0@q=BmQ0{8QF?fyD#?kI0g(L@VIZxQVUtv4 zvq@Af;TjoVk@$*2Y$}YWe4AgB_?j@^l1X$@J5wk-Po|{Wm?^F__&pQcz`fCdwd@c^ zT`(2_kKY^F&J=o!xcb&WK|VK`T5xdwZRnXS&6kiur?6tDwvxU<7Cb?5p$r03www)G)IIzJJpF6s zCr?lkKK^(Df_YtLK8aOaD?2|)Q~1`EuDs40D$YKMOOkfxq`dJI^vPNoT}&Oh_)sw& zMlriYiBi`RisIT~B}$fFE1~YOm^-D4EHtK8-SC&zvmq0wb17$j0);ao5V>(wvJxY z1b+MEH4Uu#aTZv$Mh3y!s*UJKnaac}Lkj|q_<0nu6**do!SSBpSdNoy)7Tr01-;zA7}A9oc|);QCN;Mmg7DwUPhkK#0d@SP`NNCHOv=rTouhl zTn{6i);N}PhGVg73V@MCk-;MGd0Hvz6xO=wjq?uQ%X zu~Kjavn*AR5pywrSU)9paR*sIcHkH>mpX^Q0xPwPId)OXRY$lAHqjEhu|1{T}d+keI`PTR#9?lfz@ zLbqW)B3jVa3xE}t@mF^7rCof*0R0z$4KRkkw~O!W;(M-=3upj0(6|N`1 z;ucp$FIC7JEmfRex)fu;=3VR*i=1My697LhMIYQ~rBf_(3dvQ~mU)LQT;?72MSg(w zqRI$x7%w@!!@lekFFD1_3}3zsC=lLz%_&}Wir2X6J9LFo$dhDL1+#Z>2xJFhAc<@< z+l`%0z8O_G#ZITFVE74Ak-1#bzrgYv5@g~oaLOr8I>jjl=)4^4!*$?1zrGUZxoX35 zwd_ZhW7%=>xa50-g_hVA0LEqJ2dDVnDSl7`a24(|c!q`CuHU%o%nHixfg83hg#M`rb$QsXvKxOn`Bs7aufJ6O7l2CGf-Zr3CD98p)y4OWX`BWorn#8dl@t|% zqY9~D(>WUqRbyAuV4S1pR#N(1J#V?N8<)6*hb5bRkVvgH?Ah5=2bE-xx^(G+^gyU!eg+@Ewc9n&+(~#QZ{=I#uHqY&)qZpFD~&54{tq3V+$)!rm1dFJk2epy2UhHY9q~E z>BiG;FaGInf&ZR%v#)mszdoAbhM?k=wwp8RXSu~px0vMyFS$UxJ%@kxYFV2G1fXUq(8>R_R_x?SZ%3I)uSy%Ju6A{$lyg zIs|gJ%E(tR^!|$Ouh3Kt;k9$GQfl1Rdoo^N%{gFo@-JDGYWO*UD4G5mLg?G&=bK?n zZIyR6Q%pQo22}cd@BxUSXs}S#k2A@P^%Q^j+PgrX0GNvU$ibkcpm(OdUk(ip;K?RhKcFY0UqQOB}%Y|IMX*-ccWJp*s8- zT1E}|vt1cw)%m;*XBUCqr&TT-&np%eSSR0}b@Ponc+{eUCr%Mkgjok8v*c;Hu8evI z9jk*705lWIfm`Xpu-!EQdOij6T^C6M^W-F$dGxB3Tajh6US8Qsc>(8=u{yyB$0lu~ zrSzIC-$pfSpG<~7Ct9DTnP12A6&p7|73@Xg1V&cBGNd*}noY!pdEO!X){+sJDo<{Q zn_-a**@5W9n=)$$m^)9l-9g#%+nq4I`K3m_EU2J4kibazs%eV+UCesdud$sAr?&KF2NDc0doEol!Fx~_Yx9{5qC*5 zuO}n;a@=lIGs|Se>ohgePX>NDkGB!-SNgm1mDj0L`~kj30ZXva8oHy6z)uYo;kO*y zLU)9{LD4xI38Z$!a2<;{0*$A4oe-i2H#?)Qa}odc0soAY+h)FZQg(d zugOhs@YS>8+#A$M3p!1$3@nCC|F^91CdI~_A!Hp1TMe7dq_NnrHvKH=w@CJTlbVO( zEk9yc1NdhJZThQni>q~KzA-(ZSSkT+8)({#;F#@^gDVrI!%VA z2Eu)aaVEA_W8H-m$O-4sK@Yb#NVVZU?9p$N?D7^A*=afKE$T~w^3Yq9-hzS1b01N$ zR)8T8-b=NiyB!nJagVs$pDCN&5p_O-yjU-mTB;r6qJWHJEmcz_ysDYlE5dF973miU z4m5lzO2uyqn6df=S$>9ARr&B_36o?ui}SUP0M`E`Ip{1E({cI5St!5~nfEU2>euA3 zcj3&rAeX-jJ%378yi3iCkF!kb3pE3Rrzn9OZp6=nVVTW~#~>@b9atvUw>Llqp2f5` z*yd&_R+~|MVrq*tlT?o%DBf(OzI};r!v78X04w=7s37xVF@|6;Fh3ut@rgUq`t}%r zcbV#oE#%1p|Etzg;hnSAXk z%BD^K318Q9Q)VSLyZjA5#7Qs7fcGdlaFJF7bjatZ$U6u9-g+)x&e=Q;jN%FO4)u)Y zNdsOCYcrQphXj)*m}d^!igL+jZmoyjP#XGtjT0kn`gClV2lNGU$NR`yT_o!wF+3y& zL!&Q~jlDDYQ-tf6$i1IZ5tgOeXH+A3nP%ELVdlk#1F{J|faShj#~XL-XEXw0{OM;n zWtPc5KSLty89Dj_-5@E4UId4)$ypa^D?S>2POl;OfBAFl%WE>{3+%+@^6f96@%PJH zU(j$`Q8DBa>@Qj=FI>iKpOqNBw!o1j~&btP7@D~q)h&SV&f&OVlG2aJYiTNNTg;4nI7aXb@_oZ z;?`=ZvCWHng8PJgosRn``C5A81&CA{L1TUShB7=9zS$6Jt|73Fek4b6c+P zB(RVVN-*vI32Cry9A=4{kZkZHj<+Qh1Ae4oE-?Dobt*~xJJLMJb_{n=oRUL+h3;A< zU;LH2H35erOh-{FvVjV5;9!c;YU{x*0foU+ix8g9A@InV)Ha0d1%QaCr?DPeC2QTF zx-20#;FMk^kKdreTEG`%!v7eArHLB%4^((@foeqEMx^r61-DHA58M5QORb`}3QWc- zBTzN&D-Zle|h6+@!f!8hP?29qX?8BH7%_9Ggd`V%9T$y0yQoNRA9&K0x+QXT!U zy;9w6cx*`CQ^GNMY%08S>*ch+sIwQLSIO>^pZjO=zjudOMYom2W z0^;rMn3zm$pDeL!391%@;2&A8-|t_?OGl#2jLDaDsH0 zVJk`neFrYcW)3a0SIMOkKBc*RHohu_X4;w;*VpEuh;Jopl+{sRo36@WeQ=REW~_Ps zwR5jI$K!{8R5g#gr1IP4FXS5ztyb8@FF?QY`vCps! z+}B^orh!_b?C#VeBe!U&ZnL;`h*JdkPrd2#ai`X#x}Evt4p(GeV0}hrM@mL9v_ojT5g(`oN@UYe?e-b`PZF0cii}O z3h0n68u9{dz;eu`)iik=9tBh7uPmTE{3rO1&5jj80~fIE|A(nHaBF$RyVNr9UUmx` zbOB_91MOVRnv@Yi+`b1QZ^PH>8=DPBE0>a)j@M$oa=vyQFm|TLJ^@yT5@m?IPq=Y~ zMBx(v7eO-RS8lC#xK}Db0hAREbx1>2fR-4rP~kmvL3RqzS|zZ+@aE3c7@VgLibwGL zx691|T2g&KI7FRiEx;_i5&&#!0AA90$>*YQ8~BYjH!v7Z6HBZGY7I5-QZMcLk5OO* z^8nn-jtLP~#(~2H*fqw^V(#6WutEGXpQ*N+@OCYeRfDuHS>DOJTdQ*h7ok+#z*R@a zvL0BlwF4%P<&C{MNZZ3Zu(wA`4B6;ya&pr~InAT3%~7b>pz=y9cTRPh#O$6lA=QR^ z4yFpB1F7p}=U}b8`uWenYyEY|4F$#8K%X;h4f{Zb~%^nOocx3iMz0mVBzsn&uslK8YbC+ zr_aY_Lb#UBEN&jIvE%CDaP824($P3V(a|eHD`(i?DzG6p${JO)(_H+kik6C^5vjfT zcP;#5B(}KH!u5PwknPkm*(FNr2Ti&uN{d0Z@Y_)^*Uwy#-$ZE%A-?rji@aWjM|;=* zWc1zjht}uixe={Rf>It8qqQ&Q*?C0|d+&diT9ykXwE}D57g#&*Bk!r;{l=mj#!`(I zKM;!%Q2%$SzMz$mG~%^L*)dkj@`<-gi8tT#Q#IlEr+E9OwI;|7DhQ z3-|2-+=A}e1CD?00f%o7jEmQ{)$mG^Ps`u458yl& z+JscQcOSqft@c6J1g*S|QgFq%1)If!kj2Mkk7pkFZpeJ_}+@`QEP((;QK`FUr8I;YK5u=ZLke}a;umJO(%yY zY4xl7b|iKZFSJ*?DNrw$uu=wYchEcXaFRCXZ(`RcS!@5d<>7!ew2%Ft%M<9;KBtn^ z@`R>%muF$he+c336zw1+|4E^>gCHLfUP1m&XmS4(WJAluN&{7#>~3hv=J+r8t{6(F z`=x4y_Xsss{U1UN%L(GhtPpH+d4(EN_si@5EY$x{)j<6Zq4uIKyC5^GLZq-Qi>m&| zwp?7*&zLy*UDf|_HczJgO?W|Znc7>je=5wfS-nPvrirD*QS8f`{tHA@%DMO3K1$Ib= zRxM$(2K5PV- z)6AFT!&zFIxg19|oEYAXwF(6_K9jlz1%vDbz>SSm#KtRELD;c|a2aq5ekDYn$kI}Z z6`Gs8z*@K+w{kC5)=^$Wskr4k&!gb|0N`u}ZWipDFokz0@2r?8w&C#x zo_8+hgabW1(B?@adI|%gW|J(+)`IY6YGSsQ7P9N@k`kL{GfM(I7tM-w+1dbSMNloR zYk0-{=CH&ncD2)VyLR!Ie5WJq+lBI0M{TfnF-;CA)N0$8XW%EW3$ { let stdout = ''; diff --git a/tptplus/client/src/prettyPrint/localPrettyPrintProcess.ts b/tptplus/client/src/prettyPrint/localPrettyPrintProcess.ts index 94150f4..ca73108 100644 --- a/tptplus/client/src/prettyPrint/localPrettyPrintProcess.ts +++ b/tptplus/client/src/prettyPrint/localPrettyPrintProcess.ts @@ -1,6 +1,7 @@ import * as fs from 'fs'; import * as path from 'path'; import createTPTP4X from '../../resources/wasm/tptp4X_wasm.js'; +import { isDuplicateFormulaNameError } from './prettyPrintErrors'; const WASM_DIR = path.join(__dirname, '..', '..', 'resources', 'wasm'); const WASM_BIN_PATH = path.join(WASM_DIR, 'tptp4X_wasm.wasm'); @@ -45,6 +46,10 @@ function parserDiagnosticMessage(): string | undefined { } const message = wasmDiagnostics.slice(diagnosticStart).join('\n'); + if (isDuplicateFormulaNameError(message)) { + return message.trim(); + } + const errorMatch = message.match(/^ERROR:\s*(.*)$/s); if (errorMatch) { return errorMatch[1].trim(); diff --git a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts index 0aa2efb..7d530dc 100644 --- a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts +++ b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts @@ -6,6 +6,7 @@ import { setJJParserErrorDiagnostic } from './jjParserDiagnostics'; import { formatTptpLocally } from './localPrettyPrint'; +import { isDuplicateFormulaNameError } from './prettyPrintErrors'; import { createSystemB4TptpForm } from '../systemTptpForms'; import { extractSystemB4TptpOutput, @@ -41,34 +42,46 @@ export function registerPrettyPrintCommand( // a whitespace-only file should become empty if (!sourceText.trim()) { - edit.replace(uri, fullTextRange, ""); + edit.replace(uri, fullTextRange, ''); await vscode.workspace.applyEdit(edit); return; } - // call the local pretty-printer (JJParser) + // run the local pretty-printer (JJParser) const localResult = await formatTptpLocally(context, sourceText); + if (localResult.kind === 'success') { edit.replace(uri, fullTextRange, localResult.output); await vscode.workspace.applyEdit(edit); return; } + if (localResult.kind === 'parser-error') { + if (isDuplicateFormulaNameError(localResult.message)) { + vscode.window.showErrorMessage(`Failed to format TPTP file: ${localResult.message}`); + return; + } + const errorLocation = getJJParserErrorLocation(document, localResult.message); if (errorLocation !== undefined) { setJJParserErrorDiagnostic(prettyPrintDiagnostics, document, errorLocation); await revealJJParserErrorLocation(document, errorLocation); vscode.window.showErrorMessage(`Failed to format TPTP file: ${localResult.message}`); return; - } else { - vscode.window.showWarningMessage(`\ - Failed to format TPTP file locally: ${localResult.message} - Trying the remote formatter provided by SystemB4TPTP...`); } } - // Fall back to remote pretty-printer if the local pretty-printer fails on an unknown error - // or an error that does not point to any specific location in `sourceText`. + // Fall back to remote pretty-printer if the local pretty-printer fails on a critical error, + // i.e., either an `unknown-error`, or a `parser-error` that is not a duplicate formula name + // error and does not point to any specific location in `sourceText`. + const localFailMessage = + localResult.kind === 'parser-error' ? localResult.message : 'unknown error'; + vscode.window.showWarningMessage( + `Failed to format TPTP file locally: ${localFailMessage}. ` + + 'Trying the remote formatter provided by SystemB4TPTP...' + ); + + // run the remote pretty-printer (provided by SystemB4TPTP) const form = createSystemB4TptpForm(sourceText, null); const response = await fetch('https://tptp.org/cgi-bin/SystemOnTPTPFormReply', { method: 'POST', @@ -83,13 +96,14 @@ export function registerPrettyPrintCommand( const errorLocation = getJJParserErrorLocation(document, lastLine); setJJParserErrorDiagnostic(prettyPrintDiagnostics, document, errorLocation); await revealJJParserErrorLocation(document, errorLocation); - vscode.window.showErrorMessage(`\ - Failed to format TPTP file: \ - remote formatter provided by SystemB4TPTP exited with ${lastLine}`); + vscode.window.showErrorMessage( + 'Failed to format TPTP file: ' + + `remote formatter provided by SystemB4TPTP exited with ${lastLine}` + ); } else { edit.replace(uri, fullTextRange, formattedOutput); await vscode.workspace.applyEdit(edit); - vscode.window.showInformationMessage("Format TPTP file successful."); + vscode.window.showInformationMessage('Format TPTP file successful.'); } } diff --git a/tptplus/client/src/prettyPrint/prettyPrintErrors.ts b/tptplus/client/src/prettyPrint/prettyPrintErrors.ts new file mode 100644 index 0000000..74ef799 --- /dev/null +++ b/tptplus/client/src/prettyPrint/prettyPrintErrors.ts @@ -0,0 +1,6 @@ +export const DUPLICATE_FORMULA_NAME_ERROR_PREFIX = + 'ERROR: Duplicate annotated formula name'; + +export function isDuplicateFormulaNameError(message: string): boolean { + return message.trim().startsWith(DUPLICATE_FORMULA_NAME_ERROR_PREFIX); +} diff --git a/tptplus/native/tptp-pretty/src/tptp4X_api.c b/tptplus/native/tptp-pretty/src/tptp4X_api.c index 267c073..f62cf3e 100644 --- a/tptplus/native/tptp-pretty/src/tptp4X_api.c +++ b/tptplus/native/tptp-pretty/src/tptp4X_api.c @@ -20,6 +20,8 @@ typedef struct { READFILE InputStream; SIGNATURE Signature; ANNOTATEDFORMULA AnnotatedFormula; + char * NamesBuffer; + int NamesBufferSize; FILE * OutputStream; char * OutputBuffer; size_t OutputLength; @@ -51,6 +53,24 @@ ThisNodeType != blank_line) { return(1); } +// Mirror `CheckOneDuplicateName` in NumberNames.c of TPTP4X +// TODO: improve time complexity? perhaps using ANTLR-based parser? +static int CheckOneDuplicateNameLikeTptp4X(TPTP4XPrettyState * State) { + + char * Name; + + if ((Name = GetName(State->AnnotatedFormula, NULL)) != NULL) { + if (NameInList(Name, State->NamesBuffer)) { + printf("ERROR: Duplicate annotated formula name \"%s\"\n", Name); + fflush(stdout); + return(0); + } + ExtendString(&(State->NamesBuffer), Name, &(State->NamesBufferSize)); + ExtendString(&(State->NamesBuffer), "\n", &(State->NamesBufferSize)); + } + return(1); +} + // This runs on normal returns only. Fatal JJParser errors exit the disposable // child process before control reaches this cleanup path. static void CleanupPrettyState(TPTP4XPrettyState * State) { @@ -70,6 +90,9 @@ static void CleanupPrettyState(TPTP4XPrettyState * State) { if (State->OutputStream != NULL) { fclose(State->OutputStream); } + if (State->NamesBuffer != NULL) { + Free((void **)&(State->NamesBuffer)); + } free(State->OutputBuffer); free(State); } @@ -116,6 +139,9 @@ char * tptp4x_pretty_print_tptp(const char * Input) { NextToken(State->InputStream); State->Signature = NewSignature(); LastNodeType = nontype; + State->NamesBuffer = (char *)Malloc(sizeof(String)); + State->NamesBuffer[0] = '\0'; + State->NamesBufferSize = sizeof(String); // Reading formulae one-by-one while (!CheckTokenType(State->InputStream, endeof)) { @@ -123,6 +149,9 @@ char * tptp4x_pretty_print_tptp(const char * Input) { if (State->AnnotatedFormula == NULL) { goto finish; } + if (!CheckOneDuplicateNameLikeTptp4X(State)) { + goto finish; + } if (!PrintAnnotatedFormulaLikeFtptp(State, &LastNodeType)) { goto finish; } From ddfc5eb2edd495e87d5d33f56622e519fa840cd4 Mon Sep 17 00:00:00 2001 From: jzxia Date: Thu, 9 Jul 2026 19:49:46 +0800 Subject: [PATCH 13/14] chore: publish v0.1.11: Added title-menu button for "TPTP: Check Syntax and Format TPTP File"; improved error handling for pretty-printer. --- README.md | 8 ++++++-- tptplus/CHANGELOG.md | 5 +++-- tptplus/README.md | 8 ++++++-- tptplus/package-lock.json | 8 ++++---- tptplus/package.json | 2 +- 5 files changed, 20 insertions(+), 11 deletions(-) diff --git a/README.md b/README.md index b0641f4..bfd5baa 100644 --- a/README.md +++ b/README.md @@ -158,13 +158,17 @@ Fixed issue where some greater-than-signs are not handled correctly by command " ### 0.1.9 -Added local pretty printer so that "Format TPTP File" works without Internet connection. -The original remote pretty printer is kept as a fallback. +Added local pretty-printer so that "Format TPTP File" works without Internet connection. +The original remote pretty-printer is kept as a fallback. ### 0.1.10 Added error handling for "Format TPTP File": display error message and jump to position of syntax error. +### 0.1.11 + +Added title-menu button for "TPTP: Check Syntax and Format TPTP File"; improved error handling for pretty-printer. + --- ## For TPTP Language diff --git a/tptplus/CHANGELOG.md b/tptplus/CHANGELOG.md index 0438c7e..59c6fc9 100644 --- a/tptplus/CHANGELOG.md +++ b/tptplus/CHANGELOG.md @@ -21,5 +21,6 @@ - v0.1.5 Added dynamic loading of ATP systems from tptp.org by using fetch. - v0.1.7 Automated linting, and standardized releases with GitHub actions. - v0.1.8 Fixed issue where some greater-than-signs are not handled correctly by command "Format TPTP File". -- v0.1.9 Added local pretty printer so that "Format TPTP File" works without Internet connection. The original remote pretty printer is kept as a fallback. -- v0.1.10 Added error handling for "Format TPTP File": display error message and jump to position of syntax error. \ No newline at end of file +- v0.1.9 Added local pretty-printer so that "Format TPTP File" works without Internet connection. The original remote pretty-printer is kept as a fallback. +- v0.1.10 Added error handling for "Format TPTP File": display error message and jump to position of syntax error. +- v0.1.11 Added title-menu button for "TPTP: Check Syntax and Format TPTP File"; improved error handling for pretty-printer. diff --git a/tptplus/README.md b/tptplus/README.md index 033fef0..20feff2 100644 --- a/tptplus/README.md +++ b/tptplus/README.md @@ -157,13 +157,17 @@ Fixed issue where some greater-than-signs are not handled correctly by command " ### 0.1.9 -Added local pretty printer so that "Format TPTP File" works without Internet connection. -The original remote pretty printer is kept as a fallback. +Added local pretty-printer so that "Format TPTP File" works without Internet connection. +The original remote pretty-printer is kept as a fallback. ### 0.1.10 Added error handling for "Format TPTP File": display error message and jump to position of syntax error. +### 0.1.11 + +Added title-menu button for "TPTP: Check Syntax and Format TPTP File"; improved error handling for pretty-printer. + --- ## For TPTP Language diff --git a/tptplus/package-lock.json b/tptplus/package-lock.json index c720f7d..e895acd 100644 --- a/tptplus/package-lock.json +++ b/tptplus/package-lock.json @@ -1,12 +1,12 @@ { - "name": "tptpeditor", - "version": "0.1.7", + "name": "tptp", + "version": "0.1.11", "lockfileVersion": 3, "requires": true, "packages": { "": { - "name": "tptpeditor", - "version": "0.1.7", + "name": "tptp", + "version": "0.1.11", "hasInstallScript": true, "devDependencies": { "@types/node": "^16.18.34", diff --git a/tptplus/package.json b/tptplus/package.json index 97418a8..b429d2d 100644 --- a/tptplus/package.json +++ b/tptplus/package.json @@ -3,7 +3,7 @@ "displayName": "TPTP", "publisher": "TPTPWorld", "description": "Syntax highlighting, error detection, pretty-printing, and proving & processing theorems functions for TPTP language", - "version": "0.1.10", + "version": "0.1.11", "icon": "images/icons/TPTPWorld.png", "repository": { "type": "git", From c77e595cede79258e62da76a91bf641e5e7a1464 Mon Sep 17 00:00:00 2001 From: jzxia Date: Thu, 9 Jul 2026 19:55:30 +0800 Subject: [PATCH 14/14] chore: lockfile metadata update --- tptplus/client/package-lock.json | 2 -- 1 file changed, 2 deletions(-) diff --git a/tptplus/client/package-lock.json b/tptplus/client/package-lock.json index 29a3e0c..ff64661 100644 --- a/tptplus/client/package-lock.json +++ b/tptplus/client/package-lock.json @@ -109,7 +109,6 @@ "url": "https://opencollective.com/csstools" } ], - "peer": true, "engines": { "node": ">=18" }, @@ -131,7 +130,6 @@ "url": "https://opencollective.com/csstools" } ], - "peer": true, "engines": { "node": ">=18" }