From e03a20e10ace8de185cd47bc569f3217e789c9ba Mon Sep 17 00:00:00 2001 From: jzxia Date: Wed, 15 Jul 2026 20:20:45 +0800 Subject: [PATCH 01/13] refactor: pretty-print: handle whitespace-only file in `formatTptpLocally` --- tptplus/client/src/prettyPrint/localPrettyPrint.ts | 4 ++++ tptplus/client/src/prettyPrint/prettyPrintCommand.ts | 7 ------- 2 files changed, 4 insertions(+), 7 deletions(-) diff --git a/tptplus/client/src/prettyPrint/localPrettyPrint.ts b/tptplus/client/src/prettyPrint/localPrettyPrint.ts index b40cdeb..77307b2 100644 --- a/tptplus/client/src/prettyPrint/localPrettyPrint.ts +++ b/tptplus/client/src/prettyPrint/localPrettyPrint.ts @@ -38,6 +38,10 @@ export async function formatTptpLocally( // return { kind: 'parser-error', message: '(This is an error message for debugging that does not point to any specific location in source file.)' }; // return { kind: 'unknown-error' }; + if (!input.trim()) { // a whitespace-only TPTP file should become empty + return { kind: 'success', output: '' }; + } + return new Promise(resolve => { let stdout = ''; let stderr = ''; diff --git a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts index 7d530dc..e712870 100644 --- a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts +++ b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts @@ -40,13 +40,6 @@ export function registerPrettyPrintCommand( // 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; - } - // run the local pretty-printer (JJParser) const localResult = await formatTptpLocally(context, sourceText); From afc4aa0179d3f6c54e5fbd63671243fabd5a4688 Mon Sep 17 00:00:00 2001 From: jzxia Date: Wed, 15 Jul 2026 20:56:31 +0800 Subject: [PATCH 02/13] feat: improve info/warning messages for pretty-printer; on success, show info `TPTP file formatted successfully.` or `TPTP file is already formatted.` --- .../src/prettyPrint/prettyPrintCommand.ts | 49 ++++++++++++------- 1 file changed, 31 insertions(+), 18 deletions(-) diff --git a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts index e712870..e6e0e5c 100644 --- a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts +++ b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts @@ -13,6 +13,30 @@ import { lastNonemptyLine } from '../systemB4TptpOutput'; +async function applyPrettyPrintResult( + document: vscode.TextDocument, + originalText: string, + prettyPrintResult: string +): Promise { + if (originalText === prettyPrintResult) { + vscode.window.showInformationMessage('TPTP file is already formatted.'); + return; + } + + // use WorkspaceEdit to edit any URI's document, even if it's invisible + const edit = new vscode.WorkspaceEdit(); + + const fullTextRange = new vscode.Range( + document.positionAt(0), + document.positionAt(originalText.length) + ); + edit.replace(document.uri, fullTextRange, prettyPrintResult); + await vscode.workspace.applyEdit(edit); + vscode.window.showInformationMessage('TPTP file formatted successfully.'); +} + +// TODO: use the VSCode formatting API: +// https://code.visualstudio.com/blogs/2016/11/15/formatters-best-practices export function registerPrettyPrintCommand( context: vscode.ExtensionContext, prettyPrintDiagnostics: vscode.DiagnosticCollection @@ -21,7 +45,7 @@ export function registerPrettyPrintCommand( if (!uri) { const activeEditor = vscode.window.activeTextEditor; if (!activeEditor) { - vscode.window.showErrorMessage('No active TPTP file open'); + vscode.window.showErrorMessage('No TPTP file is currently open.'); return; } uri = activeEditor.document.uri; @@ -32,20 +56,12 @@ export function registerPrettyPrintCommand( 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(); // 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); + await applyPrettyPrintResult(document, sourceText, localResult.output); return; } @@ -80,23 +96,20 @@ export function registerPrettyPrintCommand( method: 'POST', body: form }); - const text = await response.text(); - const formattedOutput = extractSystemB4TptpOutput(text); + const remoteResult = extractSystemB4TptpOutput(await response.text()); - if (formattedOutput !== undefined) { - const lastLine = lastNonemptyLine(formattedOutput); + if (remoteResult !== undefined) { + const lastLine = lastNonemptyLine(remoteResult); 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}` + `the SystemB4TPTP remote pretty-printer reported ${lastLine}` ); } else { - edit.replace(uri, fullTextRange, formattedOutput); - await vscode.workspace.applyEdit(edit); - vscode.window.showInformationMessage('Format TPTP file successful.'); + await applyPrettyPrintResult(document, sourceText, remoteResult); } } From 096cc103d9fa67f5507958eac16dea8e03e8094d Mon Sep 17 00:00:00 2001 From: jzxia Date: Wed, 15 Jul 2026 21:14:25 +0800 Subject: [PATCH 03/13] fix: pretty-printer: show error when `remoteResult === undefined`; refactor --- .../src/prettyPrint/prettyPrintCommand.ts | 54 +++++++++++++------ 1 file changed, 38 insertions(+), 16 deletions(-) diff --git a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts index e6e0e5c..1713313 100644 --- a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts +++ b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts @@ -2,6 +2,7 @@ import * as vscode from "vscode"; import { getJJParserErrorLocation, + type JJParserErrorLocation, revealJJParserErrorLocation, setJJParserErrorDiagnostic } from './jjParserDiagnostics'; @@ -35,6 +36,17 @@ async function applyPrettyPrintResult( vscode.window.showInformationMessage('TPTP file formatted successfully.'); } +async function reportPrettyPrintError( + prettyPrintDiagnostics: vscode.DiagnosticCollection, + document: vscode.TextDocument, + errorLocation: JJParserErrorLocation | undefined, + errorMessage: string +): Promise { + setJJParserErrorDiagnostic(prettyPrintDiagnostics, document, errorLocation); + await revealJJParserErrorLocation(document, errorLocation); + vscode.window.showErrorMessage(errorMessage); +} + // TODO: use the VSCode formatting API: // https://code.visualstudio.com/blogs/2016/11/15/formatters-best-practices export function registerPrettyPrintCommand( @@ -73,9 +85,12 @@ export function registerPrettyPrintCommand( 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}`); + await reportPrettyPrintError( + prettyPrintDiagnostics, + document, + errorLocation, + `Failed to format TPTP file: ${localResult.message}` + ); return; } } @@ -98,19 +113,26 @@ export function registerPrettyPrintCommand( }); const remoteResult = extractSystemB4TptpOutput(await response.text()); - if (remoteResult !== undefined) { - const lastLine = lastNonemptyLine(remoteResult); - 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: ' + - `the SystemB4TPTP remote pretty-printer reported ${lastLine}` - ); - } else { - await applyPrettyPrintResult(document, sourceText, remoteResult); - } + if (remoteResult === undefined) { + vscode.window.showErrorMessage( + 'Failed to format TPTP file: ' + + 'the SystemB4TPTP remote pretty-printer failed with unknown error' + ); + return; + } + + const lastLine = lastNonemptyLine(remoteResult); + if (lastLine?.startsWith('ERROR: ')) { + const errorLocation = getJJParserErrorLocation(document, lastLine); + await reportPrettyPrintError( + prettyPrintDiagnostics, + document, + errorLocation, + 'Failed to format TPTP file: ' + + `the SystemB4TPTP remote pretty-printer reported ${lastLine}` + ); + } else { + await applyPrettyPrintResult(document, sourceText, remoteResult); } }); From 87df404adfba0056c01f54e2a3ded0006ffd89c0 Mon Sep 17 00:00:00 2001 From: jzxia Date: Wed, 15 Jul 2026 21:43:24 +0800 Subject: [PATCH 04/13] fix: pretty-printer: show error message on network error --- .../src/prettyPrint/prettyPrintCommand.ts | 44 ++++++++++++++----- 1 file changed, 32 insertions(+), 12 deletions(-) diff --git a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts index 1713313..4204acd 100644 --- a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts +++ b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts @@ -14,6 +14,7 @@ import { lastNonemptyLine } from '../systemB4TptpOutput'; +/** Applies a pretty-print result to a document and shows success info in a toast. */ async function applyPrettyPrintResult( document: vscode.TextDocument, originalText: string, @@ -36,6 +37,7 @@ async function applyPrettyPrintResult( vscode.window.showInformationMessage('TPTP file formatted successfully.'); } +/** Publishes and reveals a parser diagnostic, then shows its error message in a toast. */ async function reportPrettyPrintError( prettyPrintDiagnostics: vscode.DiagnosticCollection, document: vscode.TextDocument, @@ -47,8 +49,32 @@ async function reportPrettyPrintError( vscode.window.showErrorMessage(errorMessage); } +/** + * Formats TPTP source text using the SystemB4TPTP remote pretty-printer. + * @throws If the request fails, the response is unsuccessful, or the formatted output cannot be extracted. + */ +async function formatTptpRemotely(sourceText: string): Promise { + const form = createSystemB4TptpForm(sourceText, null); + const response = await fetch('https://tptp.org/cgi-bin/SystemOnTPTPFormReply', { + method: 'POST', + body: form + }); + + if (!response.ok) { + throw new Error(`HTTP ${response.status}: ${response.statusText || 'request failed'}`); + } + + const result = extractSystemB4TptpOutput(await response.text()); + if (result === undefined) { + throw new Error('unknown error'); + } + + return result; +} + // TODO: use the VSCode formatting API: // https://code.visualstudio.com/blogs/2016/11/15/formatters-best-practices +/** Registers the pretty-print command with local formatting and a remote fallback. */ export function registerPrettyPrintCommand( context: vscode.ExtensionContext, prettyPrintDiagnostics: vscode.DiagnosticCollection @@ -106,18 +132,12 @@ export function registerPrettyPrintCommand( ); // 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', - body: form - }); - const remoteResult = extractSystemB4TptpOutput(await response.text()); - - if (remoteResult === undefined) { - vscode.window.showErrorMessage( - 'Failed to format TPTP file: ' + - 'the SystemB4TPTP remote pretty-printer failed with unknown error' - ); + let remoteResult: string; + try { + remoteResult = await formatTptpRemotely(sourceText); + } catch (error: unknown) { + const errorMessage = error instanceof Error ? error.message : String(error); + vscode.window.showErrorMessage(`Failed to format TPTP file remotely: ${errorMessage}`); return; } From 6d1886800c81cdc88fc5573441ac531f6b07f873 Mon Sep 17 00:00:00 2001 From: jzxia Date: Wed, 15 Jul 2026 21:57:18 +0800 Subject: [PATCH 05/13] fix: pretty-printer: before applying result, check if document has not changed since formatting began (check document version) --- .../client/src/prettyPrint/prettyPrintCommand.ts | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts index 4204acd..797ff74 100644 --- a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts +++ b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts @@ -14,12 +14,20 @@ import { lastNonemptyLine } from '../systemB4TptpOutput'; -/** Applies a pretty-print result to a document and shows success info in a toast. */ +/** Applies a pretty-print result if the document has not changed since formatting began. */ async function applyPrettyPrintResult( document: vscode.TextDocument, + originalVersion: number, originalText: string, prettyPrintResult: string ): Promise { + if (document.version !== originalVersion) { + vscode.window.showWarningMessage( + 'TPTP file changed while formatting. Please run the pretty-printer again.' + ); + return; + } + if (originalText === prettyPrintResult) { vscode.window.showInformationMessage('TPTP file is already formatted.'); return; @@ -93,13 +101,14 @@ export function registerPrettyPrintCommand( prettyPrintDiagnostics.delete(uri); const document = await vscode.workspace.openTextDocument(uri); + const sourceVersion = document.version; const sourceText = document.getText(); // run the local pretty-printer (JJParser) const localResult = await formatTptpLocally(context, sourceText); if (localResult.kind === 'success') { - await applyPrettyPrintResult(document, sourceText, localResult.output); + await applyPrettyPrintResult(document, sourceVersion, sourceText, localResult.output); return; } @@ -152,7 +161,7 @@ export function registerPrettyPrintCommand( `the SystemB4TPTP remote pretty-printer reported ${lastLine}` ); } else { - await applyPrettyPrintResult(document, sourceText, remoteResult); + await applyPrettyPrintResult(document, sourceVersion, sourceText, remoteResult); } }); From 5dc8ad34a7a0ce42fc25edf84841ed9e9c6e68dd Mon Sep 17 00:00:00 2001 From: jzxia Date: Wed, 15 Jul 2026 22:03:38 +0800 Subject: [PATCH 06/13] fix: pretty-printer: handle the case where `vscode.workspace.applyEdit` returns false --- tptplus/client/src/prettyPrint/prettyPrintCommand.ts | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts index 797ff74..454df37 100644 --- a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts +++ b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts @@ -41,8 +41,13 @@ async function applyPrettyPrintResult( document.positionAt(originalText.length) ); edit.replace(document.uri, fullTextRange, prettyPrintResult); - await vscode.workspace.applyEdit(edit); - vscode.window.showInformationMessage('TPTP file formatted successfully.'); + + const isEditApplied = await vscode.workspace.applyEdit(edit); + if (!isEditApplied) { + vscode.window.showErrorMessage('Pretty-printer succeeded, but VS Code could not apply the formatted output.'); + } else { + vscode.window.showInformationMessage('TPTP file formatted successfully.'); + } } /** Publishes and reveals a parser diagnostic, then shows its error message in a toast. */ From c6f8b3d6372bbe7e418aa46a00ce5f29a8b37e08 Mon Sep 17 00:00:00 2001 From: jzxia Date: Thu, 16 Jul 2026 11:46:51 +0800 Subject: [PATCH 07/13] feat: pretty-print: prevent concurrent pretty-printer runs --- .../src/prettyPrint/prettyPrintCommand.ts | 122 ++++++++++-------- tptplus/package.json | 1 + 2 files changed, 70 insertions(+), 53 deletions(-) diff --git a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts index 454df37..369c6f0 100644 --- a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts +++ b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts @@ -14,6 +14,8 @@ import { lastNonemptyLine } from '../systemB4TptpOutput'; +const PRETTY_PRINT_RUNNING_CONTEXT_KEY = 'tptp.prettyPrintRunning'; + /** Applies a pretty-print result if the document has not changed since formatting began. */ async function applyPrettyPrintResult( document: vscode.TextDocument, @@ -92,7 +94,14 @@ export function registerPrettyPrintCommand( context: vscode.ExtensionContext, prettyPrintDiagnostics: vscode.DiagnosticCollection ): vscode.Disposable { + let prettyPrintRunning = false; + return vscode.commands.registerCommand('tptp.prettyPrint', async (uri: vscode.Uri) => { + if (prettyPrintRunning) { + vscode.window.showInformationMessage('The TPTP pretty-printer is already running.'); + return; + } + if (!uri) { const activeEditor = vscode.window.activeTextEditor; if (!activeEditor) { @@ -102,72 +111,79 @@ export function registerPrettyPrintCommand( uri = activeEditor.document.uri; } - // Clear stale parser diagnostics before each new pretty-printer run. - prettyPrintDiagnostics.delete(uri); + prettyPrintRunning = true; + try { + await vscode.commands.executeCommand('setContext', PRETTY_PRINT_RUNNING_CONTEXT_KEY, true); - const document = await vscode.workspace.openTextDocument(uri); - const sourceVersion = document.version; - const sourceText = document.getText(); + // Clear stale parser diagnostics before each new pretty-printer run. + prettyPrintDiagnostics.delete(uri); - // run the local pretty-printer (JJParser) - const localResult = await formatTptpLocally(context, sourceText); + const document = await vscode.workspace.openTextDocument(uri); + const sourceVersion = document.version; + const sourceText = document.getText(); - if (localResult.kind === 'success') { - await applyPrettyPrintResult(document, sourceVersion, sourceText, localResult.output); - return; - } + // run the local pretty-printer (JJParser) + const localResult = await formatTptpLocally(context, sourceText); - if (localResult.kind === 'parser-error') { - if (isDuplicateFormulaNameError(localResult.message)) { - vscode.window.showErrorMessage(`Failed to format TPTP file: ${localResult.message}`); + if (localResult.kind === 'success') { + await applyPrettyPrintResult(document, sourceVersion, sourceText, localResult.output); return; } - const errorLocation = getJJParserErrorLocation(document, localResult.message); - if (errorLocation !== undefined) { - await reportPrettyPrintError( - prettyPrintDiagnostics, - document, - errorLocation, - `Failed to format TPTP file: ${localResult.message}` - ); - 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) { + await reportPrettyPrintError( + prettyPrintDiagnostics, + document, + errorLocation, + `Failed to format TPTP file: ${localResult.message}` + ); + return; + } } - } - // 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( + // 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) - let remoteResult: string; - try { - remoteResult = await formatTptpRemotely(sourceText); - } catch (error: unknown) { - const errorMessage = error instanceof Error ? error.message : String(error); - vscode.window.showErrorMessage(`Failed to format TPTP file remotely: ${errorMessage}`); - return; - } + // run the remote pretty-printer (provided by SystemB4TPTP) + let remoteResult: string; + try { + remoteResult = await formatTptpRemotely(sourceText); + } catch (error: unknown) { + const errorMessage = error instanceof Error ? error.message : String(error); + vscode.window.showErrorMessage(`Failed to format TPTP file remotely: ${errorMessage}`); + return; + } - const lastLine = lastNonemptyLine(remoteResult); - if (lastLine?.startsWith('ERROR: ')) { - const errorLocation = getJJParserErrorLocation(document, lastLine); - await reportPrettyPrintError( - prettyPrintDiagnostics, - document, - errorLocation, - 'Failed to format TPTP file: ' + - `the SystemB4TPTP remote pretty-printer reported ${lastLine}` - ); - } else { - await applyPrettyPrintResult(document, sourceVersion, sourceText, remoteResult); + const lastLine = lastNonemptyLine(remoteResult); + if (lastLine?.startsWith('ERROR: ')) { + const errorLocation = getJJParserErrorLocation(document, lastLine); + await reportPrettyPrintError( + prettyPrintDiagnostics, + document, + errorLocation, + 'Failed to format TPTP file: ' + + `the SystemB4TPTP remote pretty-printer reported ${lastLine}` + ); + } else { + await applyPrettyPrintResult(document, sourceVersion, sourceText, remoteResult); + } + } finally { + prettyPrintRunning = false; + await vscode.commands.executeCommand('setContext', PRETTY_PRINT_RUNNING_CONTEXT_KEY, false); } - }); } diff --git a/tptplus/package.json b/tptplus/package.json index 1eb9490..0a778b9 100644 --- a/tptplus/package.json +++ b/tptplus/package.json @@ -57,6 +57,7 @@ { "command": "tptp.prettyPrint", "title": "TPTP: Pretty-Print TPTP File", + "enablement": "!tptp.prettyPrintRunning", "icon": { "light": "./images/icons/PrettyPrint.png", "dark": "./images/icons/PrettyPrint.png" From 790e54a867589ce8476aa63d213faa5b3ac7711b Mon Sep 17 00:00:00 2001 From: jzxia Date: Thu, 16 Jul 2026 17:31:14 +0800 Subject: [PATCH 08/13] feat: skip redundant pretty-printer runs by tracking pretty-print state per document and reset it after edits --- tptplus/client/src/extension.ts | 12 +--- .../src/prettyPrint/prettyPrintCommand.ts | 64 ++++++++++++++++--- .../src/prettyPrint/prettyPrintState.ts | 16 +++++ 3 files changed, 72 insertions(+), 20 deletions(-) create mode 100644 tptplus/client/src/prettyPrint/prettyPrintState.ts diff --git a/tptplus/client/src/extension.ts b/tptplus/client/src/extension.ts index b2f7c29..5e6f5aa 100644 --- a/tptplus/client/src/extension.ts +++ b/tptplus/client/src/extension.ts @@ -17,14 +17,6 @@ import { registerPrettyPrintCommand } from './prettyPrint/prettyPrintCommand'; let client: LanguageClient; export function activate(context: ExtensionContext) { - const prettyPrintDiagnostics = vscode.languages.createDiagnosticCollection('tptpPrettyPrint'); - context.subscriptions.push(prettyPrintDiagnostics); - context.subscriptions.push( - vscode.workspace.onDidChangeTextDocument(event => { - prettyPrintDiagnostics.delete(event.document.uri); - }) - ); - async function fetchList(url: string, inputType: string = 'radio') { const response = await fetch(url, { "body": null, @@ -324,9 +316,7 @@ export function activate(context: ExtensionContext) { context.subscriptions.push(prepareProblem); //@ FORMAT A PROBLEM BY RUNNING JJPARSER LOCALLY, USING REMOTE SYSTEMB4TPTP AS FALLBACK - context.subscriptions.push( - registerPrettyPrintCommand(context, prettyPrintDiagnostics) - ); + context.subscriptions.push(registerPrettyPrintCommand(context)); //@ RUN A THEOREM THROUGH SYSTEMONTPTP const proveProblem = vscode.commands.registerCommand('tptp.proveProblem', async (uri: vscode.Uri) => { diff --git a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts index 369c6f0..e852c66 100644 --- a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts +++ b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts @@ -8,6 +8,10 @@ import { } from './jjParserDiagnostics'; import { formatTptpLocally } from './localPrettyPrint'; import { isDuplicateFormulaNameError } from './prettyPrintErrors'; +import { + mightNeedPrettyPrinting, + setMightNeedPrettyPrinting +} from './prettyPrintState'; import { createSystemB4TptpForm } from '../systemTptpForms'; import { extractSystemB4TptpOutput, @@ -22,17 +26,17 @@ async function applyPrettyPrintResult( originalVersion: number, originalText: string, prettyPrintResult: string -): Promise { +): Promise { if (document.version !== originalVersion) { vscode.window.showWarningMessage( 'TPTP file changed while formatting. Please run the pretty-printer again.' ); - return; + return false; } if (originalText === prettyPrintResult) { vscode.window.showInformationMessage('TPTP file is already formatted.'); - return; + return true; } // use WorkspaceEdit to edit any URI's document, even if it's invisible @@ -47,8 +51,10 @@ async function applyPrettyPrintResult( const isEditApplied = await vscode.workspace.applyEdit(edit); if (!isEditApplied) { vscode.window.showErrorMessage('Pretty-printer succeeded, but VS Code could not apply the formatted output.'); + return false; } else { vscode.window.showInformationMessage('TPTP file formatted successfully.'); + return true; } } @@ -91,12 +97,12 @@ async function formatTptpRemotely(sourceText: string): Promise { // https://code.visualstudio.com/blogs/2016/11/15/formatters-best-practices /** Registers the pretty-print command with local formatting and a remote fallback. */ export function registerPrettyPrintCommand( - context: vscode.ExtensionContext, - prettyPrintDiagnostics: vscode.DiagnosticCollection + context: vscode.ExtensionContext ): vscode.Disposable { + const prettyPrintDiagnostics = vscode.languages.createDiagnosticCollection('tptpPrettyPrint'); let prettyPrintRunning = false; - return vscode.commands.registerCommand('tptp.prettyPrint', async (uri: vscode.Uri) => { + const commandDisposable = vscode.commands.registerCommand('tptp.prettyPrint', async (uri: vscode.Uri) => { if (prettyPrintRunning) { vscode.window.showInformationMessage('The TPTP pretty-printer is already running.'); return; @@ -115,10 +121,17 @@ export function registerPrettyPrintCommand( try { await vscode.commands.executeCommand('setContext', PRETTY_PRINT_RUNNING_CONTEXT_KEY, true); + const document = await vscode.workspace.openTextDocument(uri); + if (!mightNeedPrettyPrinting(document)) { + vscode.window.showInformationMessage( + 'The file has not changed since the last pretty-printer run.' + ); + return; + } + // Clear stale parser diagnostics before each new pretty-printer run. prettyPrintDiagnostics.delete(uri); - const document = await vscode.workspace.openTextDocument(uri); const sourceVersion = document.version; const sourceText = document.getText(); @@ -126,18 +139,32 @@ export function registerPrettyPrintCommand( const localResult = await formatTptpLocally(context, sourceText); if (localResult.kind === 'success') { - await applyPrettyPrintResult(document, sourceVersion, sourceText, localResult.output); + const documentIsFormatted = await applyPrettyPrintResult( + document, + sourceVersion, + sourceText, + localResult.output + ); + if (documentIsFormatted) { + setMightNeedPrettyPrinting(document, false); + } return; } if (localResult.kind === 'parser-error') { if (isDuplicateFormulaNameError(localResult.message)) { + if (document.version === sourceVersion) { + setMightNeedPrettyPrinting(document, false); + } vscode.window.showErrorMessage(`Failed to format TPTP file: ${localResult.message}`); return; } const errorLocation = getJJParserErrorLocation(document, localResult.message); if (errorLocation !== undefined) { + if (document.version === sourceVersion) { + setMightNeedPrettyPrinting(document, false); + } await reportPrettyPrintError( prettyPrintDiagnostics, document, @@ -179,11 +206,30 @@ export function registerPrettyPrintCommand( `the SystemB4TPTP remote pretty-printer reported ${lastLine}` ); } else { - await applyPrettyPrintResult(document, sourceVersion, sourceText, remoteResult); + const documentIsFormatted = await applyPrettyPrintResult( + document, + sourceVersion, + sourceText, + remoteResult + ); + if (documentIsFormatted) { + setMightNeedPrettyPrinting(document, false); + } } } finally { prettyPrintRunning = false; await vscode.commands.executeCommand('setContext', PRETTY_PRINT_RUNNING_CONTEXT_KEY, false); } }); + + const changeDisposable = vscode.workspace.onDidChangeTextDocument(event => { + prettyPrintDiagnostics.delete(event.document.uri); + setMightNeedPrettyPrinting(event.document, true); + }); + + return vscode.Disposable.from( + prettyPrintDiagnostics, + commandDisposable, + changeDisposable + ); } diff --git a/tptplus/client/src/prettyPrint/prettyPrintState.ts b/tptplus/client/src/prettyPrint/prettyPrintState.ts new file mode 100644 index 0000000..2587859 --- /dev/null +++ b/tptplus/client/src/prettyPrint/prettyPrintState.ts @@ -0,0 +1,16 @@ +import type * as vscode from 'vscode'; + +const mightNeedPrettyPrintingByDocument = new WeakMap(); + +/** Whether the current contents of a document might need to be pretty-printed. */ +export function mightNeedPrettyPrinting(document: vscode.TextDocument): boolean { + return mightNeedPrettyPrintingByDocument.get(document) ?? true; +} + +/** Records whether the current contents of a document might need to be pretty-printed. */ +export function setMightNeedPrettyPrinting( + document: vscode.TextDocument, + mightNeedPrettyPrinting: boolean +): void { + mightNeedPrettyPrintingByDocument.set(document, mightNeedPrettyPrinting); +} From 32ac3318b4f7e239bfbd14990267a45ff4d80a48 Mon Sep 17 00:00:00 2001 From: jzxia Date: Fri, 17 Jul 2026 19:38:54 +0800 Subject: [PATCH 09/13] refactor(pretty-print): separate workflow from VS Code command; track completed formatting attempts by document version; normalize local and remote formatter outcomes --- .../client/src/prettyPrint/jjParserErrors.ts | 43 +++ .../src/prettyPrint/localPrettyPrint.ts | 24 +- .../prettyPrint/localPrettyPrintProcess.ts | 4 +- .../src/prettyPrint/prettyPrintCommand.ts | 340 ++++++++---------- ...agnostics.ts => prettyPrintDiagnostics.ts} | 46 +-- .../src/prettyPrint/prettyPrintErrors.ts | 6 - .../src/prettyPrint/prettyPrintState.ts | 17 +- .../src/prettyPrint/prettyPrintTypes.ts | 38 ++ .../src/prettyPrint/prettyPrintWorkflow.ts | 96 +++++ .../src/prettyPrint/remotePrettyPrint.ts | 45 +++ 10 files changed, 417 insertions(+), 242 deletions(-) create mode 100644 tptplus/client/src/prettyPrint/jjParserErrors.ts rename tptplus/client/src/prettyPrint/{jjParserDiagnostics.ts => prettyPrintDiagnostics.ts} (63%) delete mode 100644 tptplus/client/src/prettyPrint/prettyPrintErrors.ts create mode 100644 tptplus/client/src/prettyPrint/prettyPrintTypes.ts create mode 100644 tptplus/client/src/prettyPrint/prettyPrintWorkflow.ts create mode 100644 tptplus/client/src/prettyPrint/remotePrettyPrint.ts diff --git a/tptplus/client/src/prettyPrint/jjParserErrors.ts b/tptplus/client/src/prettyPrint/jjParserErrors.ts new file mode 100644 index 0000000..efc0f34 --- /dev/null +++ b/tptplus/client/src/prettyPrint/jjParserErrors.ts @@ -0,0 +1,43 @@ +import type { PrettyPrintSourceErrorLocation } from './prettyPrintTypes'; + +const DUPLICATE_FORMULA_NAME_ERROR_PREFIX = + 'ERROR: Duplicate annotated formula name'; + +export type ParsedJJParserError = + | { kind: 'duplicate-name' } + | { kind: 'syntax-error'; location: PrettyPrintSourceErrorLocation } + | { kind: 'unlocated-error' }; + +/** + * Classifies a JJParser error and extracts its zero-based source location when present. + * Expected located messages include: + * 'SyntaxError: Line 15 Char 6 Token "{" continuing with ...' + * 'SyntaxError: Line 11 Char 42 Character "[" continuing with ...' + */ +export function parseJJParserError(message: string): ParsedJJParserError { + if (message.trim().startsWith(DUPLICATE_FORMULA_NAME_ERROR_PREFIX)) { + return { kind: 'duplicate-name' }; + } + + const match = message.match( + /\bLine\s+(\d+)\s+Char\s+(\d+)(?:\s+(?:Token|Character)\s+"([\s\S]*?)"\s+continuing\b)?/ + ); + if (!match) { + return { kind: 'unlocated-error' }; + } + + const reportedLine = Number.parseInt(match[1], 10); + const reportedCharacter = Number.parseInt(match[2], 10); + if (Number.isNaN(reportedLine) || Number.isNaN(reportedCharacter)) { + return { kind: 'unlocated-error' }; + } + + return { + kind: 'syntax-error', + location: { + line: Math.max(0, reportedLine - 1), + character: Math.max(0, reportedCharacter - 1), + reportedText: match[3], + }, + }; +} diff --git a/tptplus/client/src/prettyPrint/localPrettyPrint.ts b/tptplus/client/src/prettyPrint/localPrettyPrint.ts index 77307b2..3bff5e7 100644 --- a/tptplus/client/src/prettyPrint/localPrettyPrint.ts +++ b/tptplus/client/src/prettyPrint/localPrettyPrint.ts @@ -1,15 +1,11 @@ import { spawn } from 'child_process'; import * as path from 'path'; -import * as vscode from 'vscode'; +import type * as vscode from 'vscode'; +import type { PrettyPrintFormatterResult } from './prettyPrintTypes'; const RUNNER_PATH = path.join('client', 'out', 'prettyPrint', 'localPrettyPrintProcess.js'); const LOCAL_PRETTY_PRINT_TIMEOUT_MS = 10000; // TODO: make this configurable -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()) { @@ -32,11 +28,11 @@ function readParserError(stderr: string): string | undefined { export async function formatTptpLocally( context: vscode.ExtensionContext, input: string -): Promise { +): 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 { kind: 'unknown-error' }; + // return { kind: 'source-error', message: '(This is an error message for debugging that does not point to any specific location in source file.)' }; + // return { kind: 'failure', message: 'unknown error' }; if (!input.trim()) { // a whitespace-only TPTP file should become empty return { kind: 'success', output: '' }; @@ -54,7 +50,7 @@ export async function formatTptpLocally( stdio: ['pipe', 'pipe', 'pipe'], // stdin, stdout, stderr }); - function finish(result: LocalPrettyPrintResult): void { + function finish(result: PrettyPrintFormatterResult): void { if (settled) return; settled = true; clearTimeout(timeout); @@ -64,20 +60,20 @@ export async function formatTptpLocally( const timeout = setTimeout(() => { child.kill(); finish({ - kind: 'parser-error', + kind: 'failure', message: `timeout after ${LOCAL_PRETTY_PRINT_TIMEOUT_MS} ms` }); }, LOCAL_PRETTY_PRINT_TIMEOUT_MS); - child.on('error', () => finish({ kind: 'unknown-error' })); + child.on('error', error => finish({ kind: 'failure', message: error.message })); 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' } + { kind: 'source-error', message: parserError } : + { kind: 'failure', message: 'unknown error' } ); } }); diff --git a/tptplus/client/src/prettyPrint/localPrettyPrintProcess.ts b/tptplus/client/src/prettyPrint/localPrettyPrintProcess.ts index ca73108..7096189 100644 --- a/tptplus/client/src/prettyPrint/localPrettyPrintProcess.ts +++ b/tptplus/client/src/prettyPrint/localPrettyPrintProcess.ts @@ -1,7 +1,7 @@ import * as fs from 'fs'; import * as path from 'path'; import createTPTP4X from '../../resources/wasm/tptp4X_wasm.js'; -import { isDuplicateFormulaNameError } from './prettyPrintErrors'; +import { parseJJParserError } from './jjParserErrors'; const WASM_DIR = path.join(__dirname, '..', '..', 'resources', 'wasm'); const WASM_BIN_PATH = path.join(WASM_DIR, 'tptp4X_wasm.wasm'); @@ -46,7 +46,7 @@ function parserDiagnosticMessage(): string | undefined { } const message = wasmDiagnostics.slice(diagnosticStart).join('\n'); - if (isDuplicateFormulaNameError(message)) { + if (parseJJParserError(message).kind === 'duplicate-name') { return message.trim(); } diff --git a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts index e852c66..3eb5aa6 100644 --- a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts +++ b/tptplus/client/src/prettyPrint/prettyPrintCommand.ts @@ -1,235 +1,211 @@ -import * as vscode from "vscode"; +import * as vscode from 'vscode'; import { - getJJParserErrorLocation, - type JJParserErrorLocation, + createJJParserDiagnosticLocation, revealJJParserErrorLocation, setJJParserErrorDiagnostic -} from './jjParserDiagnostics'; +} from './prettyPrintDiagnostics'; import { formatTptpLocally } from './localPrettyPrint'; -import { isDuplicateFormulaNameError } from './prettyPrintErrors'; +import { formatTptpWithFallback } from './prettyPrintWorkflow'; +import { formatTptpRemotely } from './remotePrettyPrint'; import { - mightNeedPrettyPrinting, - setMightNeedPrettyPrinting + markPrettyPrintVersionHandled, + wasPrettyPrintVersionHandled } from './prettyPrintState'; -import { createSystemB4TptpForm } from '../systemTptpForms'; -import { - extractSystemB4TptpOutput, - lastNonemptyLine -} from '../systemB4TptpOutput'; +import type { PrettyPrintOutcome } from './prettyPrintTypes'; +const PRETTY_PRINT_COMMAND = 'tptp.prettyPrint'; const PRETTY_PRINT_RUNNING_CONTEXT_KEY = 'tptp.prettyPrintRunning'; -/** Applies a pretty-print result if the document has not changed since formatting began. */ +async function setPrettyPrintRunningContext(running: boolean): Promise { + await vscode.commands.executeCommand( + 'setContext', + PRETTY_PRINT_RUNNING_CONTEXT_KEY, + running + ); +} + +function getTargetUri(uri?: vscode.Uri): vscode.Uri | undefined { + return uri ?? vscode.window.activeTextEditor?.document.uri; +} + +interface DocumentSnapshot { + version: number; + text: string; +} + +type ApplyPrettyPrintResult = 'applied' | 'rejected' | 'stale' | 'unchanged'; + +/** Applies formatted text only when the document still matches the input snapshot. */ async function applyPrettyPrintResult( document: vscode.TextDocument, - originalVersion: number, - originalText: string, - prettyPrintResult: string -): Promise { - if (document.version !== originalVersion) { - vscode.window.showWarningMessage( - 'TPTP file changed while formatting. Please run the pretty-printer again.' - ); - return false; + snapshot: DocumentSnapshot, + output: string +): Promise { + if (document.version !== snapshot.version) { + return 'stale'; } - if (originalText === prettyPrintResult) { - vscode.window.showInformationMessage('TPTP file is already formatted.'); - return true; + if (snapshot.text === output) { + return 'unchanged'; } - // use WorkspaceEdit to edit any URI's document, even if it's invisible const edit = new vscode.WorkspaceEdit(); - const fullTextRange = new vscode.Range( document.positionAt(0), - document.positionAt(originalText.length) + document.positionAt(snapshot.text.length) ); - edit.replace(document.uri, fullTextRange, prettyPrintResult); - - const isEditApplied = await vscode.workspace.applyEdit(edit); - if (!isEditApplied) { - vscode.window.showErrorMessage('Pretty-printer succeeded, but VS Code could not apply the formatted output.'); - return false; - } else { - vscode.window.showInformationMessage('TPTP file formatted successfully.'); - return true; - } + edit.replace(document.uri, fullTextRange, output); + + return await vscode.workspace.applyEdit(edit) ? 'applied' : 'rejected'; } -/** Publishes and reveals a parser diagnostic, then shows its error message in a toast. */ -async function reportPrettyPrintError( - prettyPrintDiagnostics: vscode.DiagnosticCollection, +async function reportSourceError( + diagnostics: vscode.DiagnosticCollection, document: vscode.TextDocument, - errorLocation: JJParserErrorLocation | undefined, - errorMessage: string + outcome: Extract ): Promise { - setJJParserErrorDiagnostic(prettyPrintDiagnostics, document, errorLocation); + const errorLocation = createJJParserDiagnosticLocation( + document, + outcome.message, + outcome.location + ); + setJJParserErrorDiagnostic(diagnostics, document, errorLocation); await revealJJParserErrorLocation(document, errorLocation); - vscode.window.showErrorMessage(errorMessage); + + const message = outcome.formatter === 'remote' + ? 'Failed to format TPTP file: ' + + `the SystemB4TPTP remote pretty-printer reported ${outcome.message}` + : `Failed to format TPTP file: ${outcome.message}`; + vscode.window.showErrorMessage(message); } -/** - * Formats TPTP source text using the SystemB4TPTP remote pretty-printer. - * @throws If the request fails, the response is unsuccessful, or the formatted output cannot be extracted. - */ -async function formatTptpRemotely(sourceText: string): Promise { - const form = createSystemB4TptpForm(sourceText, null); - const response = await fetch('https://tptp.org/cgi-bin/SystemOnTPTPFormReply', { - method: 'POST', - body: form - }); +async function presentPrettyPrintOutcome( + diagnostics: vscode.DiagnosticCollection, + document: vscode.TextDocument, + snapshot: DocumentSnapshot, + outcome: PrettyPrintOutcome +): Promise { + if (document.version !== snapshot.version) { + vscode.window.showWarningMessage( + 'TPTP file changed while formatting. Please run the pretty-printer again.' + ); + return; + } + + if (outcome.kind === 'source-error') { + markPrettyPrintVersionHandled(document); + await reportSourceError(diagnostics, document, outcome); + return; + } + + if (outcome.kind === 'formatter-error') { + vscode.window.showErrorMessage( + `Failed to format TPTP file ${outcome.formatter === 'remote' ? 'remotely' : 'locally'}: ` + + outcome.message + ); + return; + } - if (!response.ok) { - throw new Error(`HTTP ${response.status}: ${response.statusText || 'request failed'}`); + const applyResult = await applyPrettyPrintResult(document, snapshot, outcome.output); + switch (applyResult) { + case 'applied': + markPrettyPrintVersionHandled(document); + vscode.window.showInformationMessage('TPTP file formatted successfully.'); + return; + case 'unchanged': + markPrettyPrintVersionHandled(document); + vscode.window.showInformationMessage('TPTP file is already formatted.'); + return; + case 'stale': + vscode.window.showWarningMessage( + 'TPTP file changed while formatting. Please run the pretty-printer again.' + ); + return; + case 'rejected': + vscode.window.showErrorMessage( + 'Pretty-printer succeeded, but VS Code could not apply the formatted output.' + ); } +} - const result = extractSystemB4TptpOutput(await response.text()); - if (result === undefined) { - throw new Error('unknown error'); +async function executePrettyPrint( + context: vscode.ExtensionContext, + diagnostics: vscode.DiagnosticCollection, + uri: vscode.Uri +): Promise { + const document = await vscode.workspace.openTextDocument(uri); + if (wasPrettyPrintVersionHandled(document)) { + vscode.window.showInformationMessage( + 'The file has not changed since the last pretty-printer run.' + ); + return; } - return result; + diagnostics.delete(document.uri); + const snapshot: DocumentSnapshot = { + version: document.version, + text: document.getText(), + }; + + const outcome = await formatTptpWithFallback(snapshot.text, { + formatLocally: sourceText => formatTptpLocally(context, sourceText), + formatRemotely: formatTptpRemotely, + onRemoteFallback: localFailureMessage => { + vscode.window.showWarningMessage( + `Failed to format TPTP file locally: ${localFailureMessage}. ` + + 'Trying the remote formatter provided by SystemB4TPTP...' + ); + }, + }); + + await presentPrettyPrintOutcome(diagnostics, document, snapshot, outcome); } -// TODO: use the VSCode formatting API: -// https://code.visualstudio.com/blogs/2016/11/15/formatters-best-practices -/** Registers the pretty-print command with local formatting and a remote fallback. */ -export function registerPrettyPrintCommand( - context: vscode.ExtensionContext -): vscode.Disposable { - const prettyPrintDiagnostics = vscode.languages.createDiagnosticCollection('tptpPrettyPrint'); +function createPrettyPrintCommandHandler( + context: vscode.ExtensionContext, + diagnostics: vscode.DiagnosticCollection +): (uri?: vscode.Uri) => Promise { let prettyPrintRunning = false; - const commandDisposable = vscode.commands.registerCommand('tptp.prettyPrint', async (uri: vscode.Uri) => { + return async (uri?: vscode.Uri): Promise => { if (prettyPrintRunning) { vscode.window.showInformationMessage('The TPTP pretty-printer is already running.'); return; } - if (!uri) { - const activeEditor = vscode.window.activeTextEditor; - if (!activeEditor) { - vscode.window.showErrorMessage('No TPTP file is currently open.'); - return; - } - uri = activeEditor.document.uri; + const targetUri = getTargetUri(uri); + if (!targetUri) { + vscode.window.showErrorMessage('No TPTP file is currently open.'); + return; } prettyPrintRunning = true; try { - await vscode.commands.executeCommand('setContext', PRETTY_PRINT_RUNNING_CONTEXT_KEY, true); - - const document = await vscode.workspace.openTextDocument(uri); - if (!mightNeedPrettyPrinting(document)) { - vscode.window.showInformationMessage( - 'The file has not changed since the last pretty-printer run.' - ); - return; - } - - // Clear stale parser diagnostics before each new pretty-printer run. - prettyPrintDiagnostics.delete(uri); - - const sourceVersion = document.version; - const sourceText = document.getText(); - - // run the local pretty-printer (JJParser) - const localResult = await formatTptpLocally(context, sourceText); - - if (localResult.kind === 'success') { - const documentIsFormatted = await applyPrettyPrintResult( - document, - sourceVersion, - sourceText, - localResult.output - ); - if (documentIsFormatted) { - setMightNeedPrettyPrinting(document, false); - } - return; - } - - if (localResult.kind === 'parser-error') { - if (isDuplicateFormulaNameError(localResult.message)) { - if (document.version === sourceVersion) { - setMightNeedPrettyPrinting(document, false); - } - vscode.window.showErrorMessage(`Failed to format TPTP file: ${localResult.message}`); - return; - } - - const errorLocation = getJJParserErrorLocation(document, localResult.message); - if (errorLocation !== undefined) { - if (document.version === sourceVersion) { - setMightNeedPrettyPrinting(document, false); - } - await reportPrettyPrintError( - prettyPrintDiagnostics, - document, - errorLocation, - `Failed to format TPTP file: ${localResult.message}` - ); - return; - } - } - - // 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) - let remoteResult: string; - try { - remoteResult = await formatTptpRemotely(sourceText); - } catch (error: unknown) { - const errorMessage = error instanceof Error ? error.message : String(error); - vscode.window.showErrorMessage(`Failed to format TPTP file remotely: ${errorMessage}`); - return; - } - - const lastLine = lastNonemptyLine(remoteResult); - if (lastLine?.startsWith('ERROR: ')) { - const errorLocation = getJJParserErrorLocation(document, lastLine); - await reportPrettyPrintError( - prettyPrintDiagnostics, - document, - errorLocation, - 'Failed to format TPTP file: ' + - `the SystemB4TPTP remote pretty-printer reported ${lastLine}` - ); - } else { - const documentIsFormatted = await applyPrettyPrintResult( - document, - sourceVersion, - sourceText, - remoteResult - ); - if (documentIsFormatted) { - setMightNeedPrettyPrinting(document, false); - } - } + await setPrettyPrintRunningContext(true); + await executePrettyPrint(context, diagnostics, targetUri); + } catch (error: unknown) { + const message = error instanceof Error ? error.message : String(error); + vscode.window.showErrorMessage(`Failed to format TPTP file: ${message}`); } finally { + await setPrettyPrintRunningContext(false); prettyPrintRunning = false; - await vscode.commands.executeCommand('setContext', PRETTY_PRINT_RUNNING_CONTEXT_KEY, false); } - }); + }; +} - const changeDisposable = vscode.workspace.onDidChangeTextDocument(event => { - prettyPrintDiagnostics.delete(event.document.uri); - setMightNeedPrettyPrinting(event.document, true); - }); +/** Registers the pretty-print command and its diagnostic lifecycle. */ +export function registerPrettyPrintCommand( + context: vscode.ExtensionContext +): vscode.Disposable { + const diagnostics = vscode.languages.createDiagnosticCollection('tptpPrettyPrint'); + const commandHandler = createPrettyPrintCommandHandler(context, diagnostics); return vscode.Disposable.from( - prettyPrintDiagnostics, - commandDisposable, - changeDisposable + diagnostics, + vscode.commands.registerCommand(PRETTY_PRINT_COMMAND, commandHandler), + vscode.workspace.onDidChangeTextDocument(event => { + diagnostics.delete(event.document.uri); + }) ); } diff --git a/tptplus/client/src/prettyPrint/jjParserDiagnostics.ts b/tptplus/client/src/prettyPrint/prettyPrintDiagnostics.ts similarity index 63% rename from tptplus/client/src/prettyPrint/jjParserDiagnostics.ts rename to tptplus/client/src/prettyPrint/prettyPrintDiagnostics.ts index 189813b..dacce26 100644 --- a/tptplus/client/src/prettyPrint/jjParserDiagnostics.ts +++ b/tptplus/client/src/prettyPrint/prettyPrintDiagnostics.ts @@ -1,37 +1,27 @@ -import * as vscode from "vscode"; +import * as vscode from 'vscode'; +import type { PrettyPrintSourceErrorLocation } from './prettyPrintTypes'; -export interface JJParserErrorLocation { +export interface PrettyPrintDiagnosticLocation { 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)) { +/** Converts a parsed source location into a document-clamped VS Code location. */ +export function createJJParserDiagnosticLocation( + document: vscode.TextDocument, + message: string, + sourceLocation: PrettyPrintSourceErrorLocation | undefined +): PrettyPrintDiagnosticLocation | undefined { + if (!sourceLocation) { return undefined; } - const lineIndex = Math.max(0, Math.min(reportedLine - 1, document.lineCount - 1)); + const lineIndex = Math.min(sourceLocation.line, document.lineCount - 1); const lineText = document.lineAt(lineIndex).text; - let characterIndex = Math.max(0, Math.min(reportedCharacter - 1, lineText.length)); - const reportedText = match[3]; + let characterIndex = Math.min(sourceLocation.character, lineText.length); + const reportedText = sourceLocation.reportedText; // If the error message reports a token or character, try to move cursor to its beginning. if (reportedText) { @@ -50,8 +40,8 @@ export function getJJParserErrorLocation(document: vscode.TextDocument, message: return { position: startPosition, range: new vscode.Range(startPosition, endPosition), - message: message, - reportedText: reportedText + message, + reportedText }; } @@ -63,8 +53,8 @@ export function getJJParserErrorLocation(document: vscode.TextDocument, message: export function setJJParserErrorDiagnostic( diagnostics: vscode.DiagnosticCollection, document: vscode.TextDocument, - errorLocation: JJParserErrorLocation | undefined -) { + errorLocation: PrettyPrintDiagnosticLocation | undefined +): void { if (!errorLocation?.reportedText) { return; } @@ -85,7 +75,7 @@ export function setJJParserErrorDiagnostic( */ export async function revealJJParserErrorLocation( document: vscode.TextDocument, - errorLocation: JJParserErrorLocation | undefined + errorLocation: PrettyPrintDiagnosticLocation | undefined ): Promise { const position = errorLocation?.position; diff --git a/tptplus/client/src/prettyPrint/prettyPrintErrors.ts b/tptplus/client/src/prettyPrint/prettyPrintErrors.ts deleted file mode 100644 index 74ef799..0000000 --- a/tptplus/client/src/prettyPrint/prettyPrintErrors.ts +++ /dev/null @@ -1,6 +0,0 @@ -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/client/src/prettyPrint/prettyPrintState.ts b/tptplus/client/src/prettyPrint/prettyPrintState.ts index 2587859..e8399f3 100644 --- a/tptplus/client/src/prettyPrint/prettyPrintState.ts +++ b/tptplus/client/src/prettyPrint/prettyPrintState.ts @@ -1,16 +1,13 @@ import type * as vscode from 'vscode'; -const mightNeedPrettyPrintingByDocument = new WeakMap(); +const handledVersionByDocument = new WeakMap(); -/** Whether the current contents of a document might need to be pretty-printed. */ -export function mightNeedPrettyPrinting(document: vscode.TextDocument): boolean { - return mightNeedPrettyPrintingByDocument.get(document) ?? true; +/** Whether the current document version already produced a terminal outcome. */ +export function wasPrettyPrintVersionHandled(document: vscode.TextDocument): boolean { + return handledVersionByDocument.get(document) === document.version; } -/** Records whether the current contents of a document might need to be pretty-printed. */ -export function setMightNeedPrettyPrinting( - document: vscode.TextDocument, - mightNeedPrettyPrinting: boolean -): void { - mightNeedPrettyPrintingByDocument.set(document, mightNeedPrettyPrinting); +/** Records the current document version as having produced a terminal outcome. */ +export function markPrettyPrintVersionHandled(document: vscode.TextDocument): void { + handledVersionByDocument.set(document, document.version); } diff --git a/tptplus/client/src/prettyPrint/prettyPrintTypes.ts b/tptplus/client/src/prettyPrint/prettyPrintTypes.ts new file mode 100644 index 0000000..ff79703 --- /dev/null +++ b/tptplus/client/src/prettyPrint/prettyPrintTypes.ts @@ -0,0 +1,38 @@ +/** The formatter implementation that produced an outcome. */ +export type PrettyPrintFormatter = 'local' | 'remote'; + +/** A zero-based source location reported by a TPTP parser. */ +export interface PrettyPrintSourceErrorLocation { + line: number; + character: number; + reportedText?: string; +} + +/** The normalized result returned by an individual formatter adapter (e.g., local or remote JJParser). */ +export type PrettyPrintFormatterResult = + | { kind: 'success'; output: string } + | { kind: 'source-error'; message: string } + | { kind: 'failure'; message: string }; + +/** The result of applying the local-first, remote-fallback formatting policy. */ +export type PrettyPrintOutcome = + | { + kind: 'formatted'; + output: string; + formatter: PrettyPrintFormatter; + } + | { + kind: 'source-error'; + message: string; + location?: PrettyPrintSourceErrorLocation; + formatter: PrettyPrintFormatter; + } + | { + kind: 'formatter-error'; + message: string; + formatter: PrettyPrintFormatter; + }; + +export type PrettyPrintFormatterFunction = ( + sourceText: string +) => Promise; diff --git a/tptplus/client/src/prettyPrint/prettyPrintWorkflow.ts b/tptplus/client/src/prettyPrint/prettyPrintWorkflow.ts new file mode 100644 index 0000000..5d1fa16 --- /dev/null +++ b/tptplus/client/src/prettyPrint/prettyPrintWorkflow.ts @@ -0,0 +1,96 @@ +import { + parseJJParserError, + type ParsedJJParserError +} from './jjParserErrors'; +import type { + PrettyPrintFormatter, + PrettyPrintFormatterFunction, + PrettyPrintFormatterResult, + PrettyPrintOutcome +} from './prettyPrintTypes'; + +export interface PrettyPrintWorkflowDependencies { + formatLocally: PrettyPrintFormatterFunction; + formatRemotely: PrettyPrintFormatterFunction; + onRemoteFallback?(localFailureMessage: string): void | Promise; +} + +function errorMessage(error: unknown): string { + return error instanceof Error ? error.message : String(error); +} + +/** Ensures an adapter exception is represented by the same result type as other failures. */ +async function callFormatter( + formatter: PrettyPrintFormatterFunction, + sourceText: string +): Promise { + try { + return await formatter(sourceText); + } catch (error: unknown) { + return { kind: 'failure', message: errorMessage(error) }; + } +} + +function sourceErrorOutcome( + formatter: PrettyPrintFormatter, + message: string, + parsedError: ParsedJJParserError +): PrettyPrintOutcome { + return { + kind: 'source-error', + formatter, + message, + location: parsedError.kind === 'syntax-error' ? parsedError.location : undefined, + }; +} + +/** + * Formats source locally when possible, falling back to SystemB4TPTP only when + * the local formatter cannot produce a result or an actionable source error. + */ +export async function formatTptpWithFallback( + sourceText: string, + dependencies: PrettyPrintWorkflowDependencies +): Promise { + const localResult = await callFormatter(dependencies.formatLocally, sourceText); + + if (localResult.kind === 'success') { + return { + kind: 'formatted', + formatter: 'local', + output: localResult.output, + }; + } + + if (localResult.kind === 'source-error') { + const parsedError = parseJJParserError(localResult.message); + if (parsedError.kind !== 'unlocated-error') { + return sourceErrorOutcome('local', localResult.message, parsedError); + } + } + + await dependencies.onRemoteFallback?.(localResult.message); + const remoteResult = await callFormatter(dependencies.formatRemotely, sourceText); + + if (remoteResult.kind === 'success') { + return { + kind: 'formatted', + formatter: 'remote', + output: remoteResult.output, + }; + } + + if (remoteResult.kind === 'source-error') { + return sourceErrorOutcome( + 'remote', + remoteResult.message, + parseJJParserError(remoteResult.message) + ); + } + + return { + kind: 'formatter-error', + formatter: 'remote', + message: remoteResult.message, + }; +} diff --git a/tptplus/client/src/prettyPrint/remotePrettyPrint.ts b/tptplus/client/src/prettyPrint/remotePrettyPrint.ts new file mode 100644 index 0000000..bb926f0 --- /dev/null +++ b/tptplus/client/src/prettyPrint/remotePrettyPrint.ts @@ -0,0 +1,45 @@ +import { + extractSystemB4TptpOutput, + lastNonemptyLine +} from '../systemB4TptpOutput'; +import { createSystemB4TptpForm } from '../systemTptpForms'; +import type { PrettyPrintFormatterResult } from './prettyPrintTypes'; + +const SYSTEM_ON_TPTP_URL = 'https://tptp.org/cgi-bin/SystemOnTPTPFormReply'; + +function errorMessage(error: unknown): string { + return error instanceof Error ? error.message : String(error); +} + +/** Formats TPTP source using the SystemB4TPTP remote pretty-printer. */ +export async function formatTptpRemotely( + sourceText: string +): Promise { + try { + const response = await fetch(SYSTEM_ON_TPTP_URL, { + method: 'POST', + body: createSystemB4TptpForm(sourceText, null) + }); + + if (!response.ok) { + return { + kind: 'failure', + message: `HTTP ${response.status}: ${response.statusText || 'request failed'}`, + }; + } + + const output = extractSystemB4TptpOutput(await response.text()); + if (output === undefined) { + return { kind: 'failure', message: 'unrecognized response' }; + } + + const lastLine = lastNonemptyLine(output); + if (lastLine?.startsWith('ERROR: ')) { + return { kind: 'source-error', message: lastLine }; + } + + return { kind: 'success', output }; + } catch (error: unknown) { + return { kind: 'failure', message: errorMessage(error) }; + } +} From a0d8ba1527974ef39be62f1d1e1d8c33ea47b644 Mon Sep 17 00:00:00 2001 From: jzxia Date: Fri, 17 Jul 2026 19:52:04 +0800 Subject: [PATCH 10/13] refactor(pretty-print): shorten file names and add comments --- tptplus/client/resources/wasm/tptp4X_wasm.d.ts | 2 +- tptplus/client/src/extension.ts | 2 +- .../{prettyPrintCommand.ts => command.ts} | 12 ++++++------ .../{prettyPrintDiagnostics.ts => diagnostics.ts} | 2 +- tptplus/client/src/prettyPrint/jjParserErrors.ts | 2 +- .../prettyPrint/{localPrettyPrint.ts => local.ts} | 4 ++-- .../{localPrettyPrintProcess.ts => localProcess.ts} | 0 .../prettyPrint/{remotePrettyPrint.ts => remote.ts} | 2 +- .../prettyPrint/{prettyPrintState.ts => state.ts} | 5 +++++ .../prettyPrint/{prettyPrintTypes.ts => types.ts} | 0 .../{prettyPrintWorkflow.ts => workflow.ts} | 2 +- 11 files changed, 19 insertions(+), 14 deletions(-) rename tptplus/client/src/prettyPrint/{prettyPrintCommand.ts => command.ts} (95%) rename tptplus/client/src/prettyPrint/{prettyPrintDiagnostics.ts => diagnostics.ts} (97%) rename tptplus/client/src/prettyPrint/{localPrettyPrint.ts => local.ts} (96%) rename tptplus/client/src/prettyPrint/{localPrettyPrintProcess.ts => localProcess.ts} (100%) rename tptplus/client/src/prettyPrint/{remotePrettyPrint.ts => remote.ts} (94%) rename tptplus/client/src/prettyPrint/{prettyPrintState.ts => state.ts} (82%) rename tptplus/client/src/prettyPrint/{prettyPrintTypes.ts => types.ts} (100%) rename tptplus/client/src/prettyPrint/{prettyPrintWorkflow.ts => workflow.ts} (98%) diff --git a/tptplus/client/resources/wasm/tptp4X_wasm.d.ts b/tptplus/client/resources/wasm/tptp4X_wasm.d.ts index d29901e..67354e3 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/prettyPrint/localPrettyPrintProcess').CreateTPTP4X; +declare const createTPTP4X: import('../../src/prettyPrint/localProcess').CreateTPTP4X; export = createTPTP4X; diff --git a/tptplus/client/src/extension.ts b/tptplus/client/src/extension.ts index 5e6f5aa..22b36a5 100644 --- a/tptplus/client/src/extension.ts +++ b/tptplus/client/src/extension.ts @@ -12,7 +12,7 @@ import { } from 'vscode-languageclient/node'; import { createSystemB4TptpForm } from './systemTptpForms'; -import { registerPrettyPrintCommand } from './prettyPrint/prettyPrintCommand'; +import { registerPrettyPrintCommand } from './prettyPrint/command'; let client: LanguageClient; diff --git a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts b/tptplus/client/src/prettyPrint/command.ts similarity index 95% rename from tptplus/client/src/prettyPrint/prettyPrintCommand.ts rename to tptplus/client/src/prettyPrint/command.ts index 3eb5aa6..535b485 100644 --- a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts +++ b/tptplus/client/src/prettyPrint/command.ts @@ -4,15 +4,15 @@ import { createJJParserDiagnosticLocation, revealJJParserErrorLocation, setJJParserErrorDiagnostic -} from './prettyPrintDiagnostics'; -import { formatTptpLocally } from './localPrettyPrint'; -import { formatTptpWithFallback } from './prettyPrintWorkflow'; -import { formatTptpRemotely } from './remotePrettyPrint'; +} from './diagnostics'; +import { formatTptpLocally } from './local'; +import { formatTptpWithFallback } from './workflow'; +import { formatTptpRemotely } from './remote'; import { markPrettyPrintVersionHandled, wasPrettyPrintVersionHandled -} from './prettyPrintState'; -import type { PrettyPrintOutcome } from './prettyPrintTypes'; +} from './state'; +import type { PrettyPrintOutcome } from './types'; const PRETTY_PRINT_COMMAND = 'tptp.prettyPrint'; const PRETTY_PRINT_RUNNING_CONTEXT_KEY = 'tptp.prettyPrintRunning'; diff --git a/tptplus/client/src/prettyPrint/prettyPrintDiagnostics.ts b/tptplus/client/src/prettyPrint/diagnostics.ts similarity index 97% rename from tptplus/client/src/prettyPrint/prettyPrintDiagnostics.ts rename to tptplus/client/src/prettyPrint/diagnostics.ts index dacce26..755edda 100644 --- a/tptplus/client/src/prettyPrint/prettyPrintDiagnostics.ts +++ b/tptplus/client/src/prettyPrint/diagnostics.ts @@ -1,5 +1,5 @@ import * as vscode from 'vscode'; -import type { PrettyPrintSourceErrorLocation } from './prettyPrintTypes'; +import type { PrettyPrintSourceErrorLocation } from './types'; export interface PrettyPrintDiagnosticLocation { position: vscode.Position; diff --git a/tptplus/client/src/prettyPrint/jjParserErrors.ts b/tptplus/client/src/prettyPrint/jjParserErrors.ts index efc0f34..41aaa8a 100644 --- a/tptplus/client/src/prettyPrint/jjParserErrors.ts +++ b/tptplus/client/src/prettyPrint/jjParserErrors.ts @@ -1,4 +1,4 @@ -import type { PrettyPrintSourceErrorLocation } from './prettyPrintTypes'; +import type { PrettyPrintSourceErrorLocation } from './types'; const DUPLICATE_FORMULA_NAME_ERROR_PREFIX = 'ERROR: Duplicate annotated formula name'; diff --git a/tptplus/client/src/prettyPrint/localPrettyPrint.ts b/tptplus/client/src/prettyPrint/local.ts similarity index 96% rename from tptplus/client/src/prettyPrint/localPrettyPrint.ts rename to tptplus/client/src/prettyPrint/local.ts index 3bff5e7..0a49359 100644 --- a/tptplus/client/src/prettyPrint/localPrettyPrint.ts +++ b/tptplus/client/src/prettyPrint/local.ts @@ -1,9 +1,9 @@ import { spawn } from 'child_process'; import * as path from 'path'; import type * as vscode from 'vscode'; -import type { PrettyPrintFormatterResult } from './prettyPrintTypes'; +import type { PrettyPrintFormatterResult } from './types'; -const RUNNER_PATH = path.join('client', 'out', 'prettyPrint', 'localPrettyPrintProcess.js'); +const RUNNER_PATH = path.join('client', 'out', 'prettyPrint', 'localProcess.js'); const LOCAL_PRETTY_PRINT_TIMEOUT_MS = 10000; // TODO: make this configurable function readParserError(stderr: string): string | undefined { diff --git a/tptplus/client/src/prettyPrint/localPrettyPrintProcess.ts b/tptplus/client/src/prettyPrint/localProcess.ts similarity index 100% rename from tptplus/client/src/prettyPrint/localPrettyPrintProcess.ts rename to tptplus/client/src/prettyPrint/localProcess.ts diff --git a/tptplus/client/src/prettyPrint/remotePrettyPrint.ts b/tptplus/client/src/prettyPrint/remote.ts similarity index 94% rename from tptplus/client/src/prettyPrint/remotePrettyPrint.ts rename to tptplus/client/src/prettyPrint/remote.ts index bb926f0..3764fa0 100644 --- a/tptplus/client/src/prettyPrint/remotePrettyPrint.ts +++ b/tptplus/client/src/prettyPrint/remote.ts @@ -3,7 +3,7 @@ import { lastNonemptyLine } from '../systemB4TptpOutput'; import { createSystemB4TptpForm } from '../systemTptpForms'; -import type { PrettyPrintFormatterResult } from './prettyPrintTypes'; +import type { PrettyPrintFormatterResult } from './types'; const SYSTEM_ON_TPTP_URL = 'https://tptp.org/cgi-bin/SystemOnTPTPFormReply'; diff --git a/tptplus/client/src/prettyPrint/prettyPrintState.ts b/tptplus/client/src/prettyPrint/state.ts similarity index 82% rename from tptplus/client/src/prettyPrint/prettyPrintState.ts rename to tptplus/client/src/prettyPrint/state.ts index e8399f3..32b5f39 100644 --- a/tptplus/client/src/prettyPrint/prettyPrintState.ts +++ b/tptplus/client/src/prettyPrint/state.ts @@ -1,3 +1,8 @@ +/** + * Tracking per-document pretty-print state so unchanged document versions can + * skip redundant pretty-print runs. + */ + import type * as vscode from 'vscode'; const handledVersionByDocument = new WeakMap(); diff --git a/tptplus/client/src/prettyPrint/prettyPrintTypes.ts b/tptplus/client/src/prettyPrint/types.ts similarity index 100% rename from tptplus/client/src/prettyPrint/prettyPrintTypes.ts rename to tptplus/client/src/prettyPrint/types.ts diff --git a/tptplus/client/src/prettyPrint/prettyPrintWorkflow.ts b/tptplus/client/src/prettyPrint/workflow.ts similarity index 98% rename from tptplus/client/src/prettyPrint/prettyPrintWorkflow.ts rename to tptplus/client/src/prettyPrint/workflow.ts index 5d1fa16..8f6c623 100644 --- a/tptplus/client/src/prettyPrint/prettyPrintWorkflow.ts +++ b/tptplus/client/src/prettyPrint/workflow.ts @@ -7,7 +7,7 @@ import type { PrettyPrintFormatterFunction, PrettyPrintFormatterResult, PrettyPrintOutcome -} from './prettyPrintTypes'; +} from './types'; export interface PrettyPrintWorkflowDependencies { formatLocally: PrettyPrintFormatterFunction; From 456b601dce876347dec92a05d6302c3636a700dd Mon Sep 17 00:00:00 2001 From: jzxia Date: Fri, 17 Jul 2026 20:01:39 +0800 Subject: [PATCH 11/13] refactor(client): reuse error message helper --- tptplus/client/src/errorMessage.ts | 4 +++ tptplus/client/src/extension.ts | 29 ++++------------------ tptplus/client/src/prettyPrint/command.ts | 4 +-- tptplus/client/src/prettyPrint/remote.ts | 5 +--- tptplus/client/src/prettyPrint/workflow.ts | 5 +--- 5 files changed, 13 insertions(+), 34 deletions(-) create mode 100644 tptplus/client/src/errorMessage.ts diff --git a/tptplus/client/src/errorMessage.ts b/tptplus/client/src/errorMessage.ts new file mode 100644 index 0000000..993fdca --- /dev/null +++ b/tptplus/client/src/errorMessage.ts @@ -0,0 +1,4 @@ +/** Returns a useful message for any value that can be thrown. */ +export function errorMessage(error: unknown): string { + return error instanceof Error ? error.message : String(error); +} diff --git a/tptplus/client/src/extension.ts b/tptplus/client/src/extension.ts index 22b36a5..9bf1887 100644 --- a/tptplus/client/src/extension.ts +++ b/tptplus/client/src/extension.ts @@ -11,6 +11,7 @@ import { TransportKind } from 'vscode-languageclient/node'; +import { errorMessage } from './errorMessage'; import { createSystemB4TptpForm } from './systemTptpForms'; import { registerPrettyPrintCommand } from './prettyPrint/command'; @@ -979,12 +980,7 @@ export function activate(context: ExtensionContext) { }); } catch (error: unknown) { - if (error instanceof Error) { - vscode.window.showErrorMessage(`Error submitting to TPTP: ${error.message}`); - } else { - // Handle cases where something else was thrown (like a string or null) - vscode.window.showErrorMessage(`Error submitting to TPTP: ${String(error)}`); - } + vscode.window.showErrorMessage(`Error submitting to TPTP: ${errorMessage(error)}`); } } }); @@ -1601,12 +1597,7 @@ export function activate(context: ExtensionContext) { }); } catch (error: unknown) { - if (error instanceof Error) { - vscode.window.showErrorMessage(`Error submitting to TPTP: ${error.message}`); - } else { - // Handle cases where something else was thrown (like a string or null) - vscode.window.showErrorMessage(`Error submitting to TPTP: ${String(error)}`); - } + vscode.window.showErrorMessage(`Error submitting to TPTP: ${errorMessage(error)}`); } } }); @@ -1939,12 +1930,7 @@ export function activate(context: ExtensionContext) { }); } catch (error: unknown) { - if (error instanceof Error) { - vscode.window.showErrorMessage(`Error submitting to TPTP: ${error.message}`); - } else { - // Handle cases where something else was thrown (like a string or null) - vscode.window.showErrorMessage(`Error submitting to TPTP: ${String(error)}`); - } + vscode.window.showErrorMessage(`Error submitting to TPTP: ${errorMessage(error)}`); } } }) @@ -2280,12 +2266,7 @@ export function activate(context: ExtensionContext) { }); } catch (error: unknown) { - if (error instanceof Error) { - vscode.window.showErrorMessage(`Error submitting to TPTP: ${error.message}`); - } else { - // Handle cases where something else was thrown (like a string or null) - vscode.window.showErrorMessage(`Error submitting to TPTP: ${String(error)}`); - } + vscode.window.showErrorMessage(`Error submitting to TPTP: ${errorMessage(error)}`); } } }) diff --git a/tptplus/client/src/prettyPrint/command.ts b/tptplus/client/src/prettyPrint/command.ts index 535b485..4fcbeb6 100644 --- a/tptplus/client/src/prettyPrint/command.ts +++ b/tptplus/client/src/prettyPrint/command.ts @@ -1,5 +1,6 @@ import * as vscode from 'vscode'; +import { errorMessage } from '../errorMessage'; import { createJJParserDiagnosticLocation, revealJJParserErrorLocation, @@ -185,8 +186,7 @@ function createPrettyPrintCommandHandler( await setPrettyPrintRunningContext(true); await executePrettyPrint(context, diagnostics, targetUri); } catch (error: unknown) { - const message = error instanceof Error ? error.message : String(error); - vscode.window.showErrorMessage(`Failed to format TPTP file: ${message}`); + vscode.window.showErrorMessage(`Failed to format TPTP file: ${errorMessage(error)}`); } finally { await setPrettyPrintRunningContext(false); prettyPrintRunning = false; diff --git a/tptplus/client/src/prettyPrint/remote.ts b/tptplus/client/src/prettyPrint/remote.ts index 3764fa0..34c10c1 100644 --- a/tptplus/client/src/prettyPrint/remote.ts +++ b/tptplus/client/src/prettyPrint/remote.ts @@ -1,3 +1,4 @@ +import { errorMessage } from '../errorMessage'; import { extractSystemB4TptpOutput, lastNonemptyLine @@ -7,10 +8,6 @@ import type { PrettyPrintFormatterResult } from './types'; const SYSTEM_ON_TPTP_URL = 'https://tptp.org/cgi-bin/SystemOnTPTPFormReply'; -function errorMessage(error: unknown): string { - return error instanceof Error ? error.message : String(error); -} - /** Formats TPTP source using the SystemB4TPTP remote pretty-printer. */ export async function formatTptpRemotely( sourceText: string diff --git a/tptplus/client/src/prettyPrint/workflow.ts b/tptplus/client/src/prettyPrint/workflow.ts index 8f6c623..f56ac37 100644 --- a/tptplus/client/src/prettyPrint/workflow.ts +++ b/tptplus/client/src/prettyPrint/workflow.ts @@ -1,3 +1,4 @@ +import { errorMessage } from '../errorMessage'; import { parseJJParserError, type ParsedJJParserError @@ -15,10 +16,6 @@ export interface PrettyPrintWorkflowDependencies { onRemoteFallback?(localFailureMessage: string): void | Promise; } -function errorMessage(error: unknown): string { - return error instanceof Error ? error.message : String(error); -} - /** Ensures an adapter exception is represented by the same result type as other failures. */ async function callFormatter( formatter: PrettyPrintFormatterFunction, From 087e6d4c81a3f67d324cb12ac3a914ef98df5946 Mon Sep 17 00:00:00 2001 From: jzxia Date: Sun, 19 Jul 2026 22:14:16 +0800 Subject: [PATCH 12/13] fix(pretty-printer): repeat source errors for unchanged files (i.e., do not skip pretty-printing for unchanged invalid files) --- tptplus/client/src/prettyPrint/command.ts | 13 ++++++------- tptplus/client/src/prettyPrint/state.ts | 18 +++++++++--------- 2 files changed, 15 insertions(+), 16 deletions(-) diff --git a/tptplus/client/src/prettyPrint/command.ts b/tptplus/client/src/prettyPrint/command.ts index 4fcbeb6..b161692 100644 --- a/tptplus/client/src/prettyPrint/command.ts +++ b/tptplus/client/src/prettyPrint/command.ts @@ -10,8 +10,8 @@ import { formatTptpLocally } from './local'; import { formatTptpWithFallback } from './workflow'; import { formatTptpRemotely } from './remote'; import { - markPrettyPrintVersionHandled, - wasPrettyPrintVersionHandled + isPrettyPrintVersionKnownFormatted, + markPrettyPrintVersionFormatted } from './state'; import type { PrettyPrintOutcome } from './types'; @@ -95,7 +95,6 @@ async function presentPrettyPrintOutcome( } if (outcome.kind === 'source-error') { - markPrettyPrintVersionHandled(document); await reportSourceError(diagnostics, document, outcome); return; } @@ -111,11 +110,11 @@ async function presentPrettyPrintOutcome( const applyResult = await applyPrettyPrintResult(document, snapshot, outcome.output); switch (applyResult) { case 'applied': - markPrettyPrintVersionHandled(document); + markPrettyPrintVersionFormatted(document); vscode.window.showInformationMessage('TPTP file formatted successfully.'); return; case 'unchanged': - markPrettyPrintVersionHandled(document); + markPrettyPrintVersionFormatted(document); vscode.window.showInformationMessage('TPTP file is already formatted.'); return; case 'stale': @@ -136,9 +135,9 @@ async function executePrettyPrint( uri: vscode.Uri ): Promise { const document = await vscode.workspace.openTextDocument(uri); - if (wasPrettyPrintVersionHandled(document)) { + if (isPrettyPrintVersionKnownFormatted(document)) { vscode.window.showInformationMessage( - 'The file has not changed since the last pretty-printer run.' + 'The file has not changed since it was last successfully formatted.' ); return; } diff --git a/tptplus/client/src/prettyPrint/state.ts b/tptplus/client/src/prettyPrint/state.ts index 32b5f39..87bfe68 100644 --- a/tptplus/client/src/prettyPrint/state.ts +++ b/tptplus/client/src/prettyPrint/state.ts @@ -1,18 +1,18 @@ /** - * Tracking per-document pretty-print state so unchanged document versions can - * skip redundant pretty-print runs. + * Tracking per-document pretty-print state so document versions already known + * to be formatted can skip redundant pretty-print runs. */ import type * as vscode from 'vscode'; -const handledVersionByDocument = new WeakMap(); +const formattedVersionByDocument = new WeakMap(); -/** Whether the current document version already produced a terminal outcome. */ -export function wasPrettyPrintVersionHandled(document: vscode.TextDocument): boolean { - return handledVersionByDocument.get(document) === document.version; +/** Whether the current document version is already known to be formatted. */ +export function isPrettyPrintVersionKnownFormatted(document: vscode.TextDocument): boolean { + return formattedVersionByDocument.get(document) === document.version; } -/** Records the current document version as having produced a terminal outcome. */ -export function markPrettyPrintVersionHandled(document: vscode.TextDocument): void { - handledVersionByDocument.set(document, document.version); +/** Records the current document version as successfully formatted. */ +export function markPrettyPrintVersionFormatted(document: vscode.TextDocument): void { + formattedVersionByDocument.set(document, document.version); } From b81812c13aa16331d9b519f85d7d370bdcfe16a2 Mon Sep 17 00:00:00 2001 From: jzxia Date: Sun, 19 Jul 2026 23:18:43 +0800 Subject: [PATCH 13/13] Retire legacy server formatting --- tptplus/client/src/extension.ts | 18 - tptplus/package.json | 4 - tptplus/server/legacy/README.md | 9 + tptplus/server/legacy/prettyPrintTPTP.ts | 462 +++++++++++++++++++++ tptplus/server/src/server.ts | 500 +---------------------- 5 files changed, 472 insertions(+), 521 deletions(-) create mode 100644 tptplus/server/legacy/README.md create mode 100644 tptplus/server/legacy/prettyPrintTPTP.ts diff --git a/tptplus/client/src/extension.ts b/tptplus/client/src/extension.ts index 9bf1887..bf1a570 100644 --- a/tptplus/client/src/extension.ts +++ b/tptplus/client/src/extension.ts @@ -2367,24 +2367,6 @@ export function activate(context: ExtensionContext) { context.subscriptions.push(importSolution); - //@ - - - //@ FORMAT DOCUMENT - let disposable = vscode.commands.registerCommand( - "tptp.formatDocument", - () => { - const editor = vscode.window.activeTextEditor; - if (editor && editor.document.languageId === "tptp") { - vscode.commands.executeCommand("editor.action.formatDocument"); - } - } - ); - - context.subscriptions.push(disposable); - - //@ - // Server is implemented in TypeScript and runs in a separate process const serverModule = context.asAbsolutePath( path.join('server', 'out', 'server.js') diff --git a/tptplus/package.json b/tptplus/package.json index 0a778b9..4ca0159 100644 --- a/tptplus/package.json +++ b/tptplus/package.json @@ -46,10 +46,6 @@ } ], "commands": [ - { - "command": "tptp.formatDocument", - "title": "TPTP: Format Document (legacy)" - }, { "command": "tptp.prepareProblem", "title": "TPTP: Prepare Problem" diff --git a/tptplus/server/legacy/README.md b/tptplus/server/legacy/README.md new file mode 100644 index 0000000..2ed024d --- /dev/null +++ b/tptplus/server/legacy/README.md @@ -0,0 +1,9 @@ +# Legacy server formatter + +`prettyPrintTPTP.ts` preserves the original heuristic formatter for historical +reference. It is intentionally outside `src`, so the TypeScript server build +does not compile or advertise it. + +The active formatter was retired because reliably identifying TPTP syntax +boundaries requires parser support. A future ANTLR-based implementation can +replace it without losing the work or context captured here. diff --git a/tptplus/server/legacy/prettyPrintTPTP.ts b/tptplus/server/legacy/prettyPrintTPTP.ts new file mode 100644 index 0000000..9ffc3ef --- /dev/null +++ b/tptplus/server/legacy/prettyPrintTPTP.ts @@ -0,0 +1,462 @@ +/** + * Legacy heuristic TPTP formatter. + * + * This implementation is intentionally kept outside `src` so it is preserved + * for reference without being compiled or advertised by the language server. + */ +export function prettyPrintTPTP(input: string): string { + const indentUnit = " "; // 4 spaces + const maxLineLength = 20; // threshold for breaking formula to new line + let indentLevel = 0; + let parenDepth = 0; // actual ( ... ) depth + let out = ""; + let inString = false; // tracking '...' or "..." + let strChar = ""; // either "'" or '"' + let inLineComment = false; + let inBlockComment = false; + let isInTPTPFormula = false; // track if we're in the formula part of TPTP declaration + let tptpCommaCount = 0; // count commas in TPTP declaration to identify formula part + let bracketDepth = 0; + let justEndedFormula = false; // track if we just ended a formula with a period + + // Helper: peek ahead, skipping any whitespace + function peekNonWhitespace(idx: number): string | null { + let j = idx; + while (j < input.length && /\s/.test(input[j])) { j++; } + return j < input.length ? input[j] : null; + } + + // Helper: check if current position is start of TPTP declaration + function isAtTPTPStart(idx: number): boolean { + const patterns = ["tpi(", "thf(", "tff(", "tcf(", "fof(", "cnf("]; + return patterns.some(pattern => input.substring(idx, idx + pattern.length) === pattern); + } + + // Helper: get the length of the TPTP declaration type + function getTPTPDeclLength(idx: number): number { + const patterns = ["tpi(", "thf(", "tff(", "tcf(", "fof(", "cnf("]; + for (const pattern of patterns) { + if (input.substring(idx, idx + pattern.length) === pattern) { + return pattern.length; + } + } + return 0; + } + + // Helper: estimate current line length from last newline + function getCurrentLineLength(): number { + const lastNewlineIdx = out.lastIndexOf('\n'); + if (lastNewlineIdx === -1) return out.length; + return out.length - lastNewlineIdx - 1; + } + + // Helper: check if there's already a blank line at the end of output + function hasBlankLineAtEnd(): boolean { + const lines = out.split('\n'); + return lines.length >= 2 && lines[lines.length - 1] === '' && lines[lines.length - 2] === ''; + } + + // Preserve empty lines by tracking consecutive newlines + function preserveEmptyLines(startIdx: number): number { + let i = startIdx; + let newlineCount = 0; + + // Count newlines (but skip other whitespace) + while (i < input.length) { + if (input[i] === '\n') { + newlineCount++; + i++; + } else if (/[ \t\r]/.test(input[i])) { + // Skip other whitespace but don't count it + i++; + } else { + break; + } + } + + // If we have more than one newline, preserve the extras as empty lines + if (newlineCount > 1) { + // Add the extra newlines (newlineCount - 1 because we already have one) + for (let j = 1; j < newlineCount && j < 3; j++) { + out += '\n'; + } + } + + return i; + } + + // We iterate char by char, but sometimes lookahead ("=>" etc.) + for (let i = 0; i < input.length; ) { + const ch = input[i]; + const next = input[i + 1] ?? ""; + + if (ch === "[") { + bracketDepth++; + out += ch; + i++; + continue; + } + + if (ch === "]") { + bracketDepth = Math.max(bracketDepth - 1, 0); + out += ch; + i++; + continue; + } + + // + // 1) Single‐line comment "% …" (only if it occurs at line‐start or after a newline) + // + if ( + !inString && + !inBlockComment && + ch === "%" && + (i === 0 || input[i - 1] === "\n") + ) { + inLineComment = true; + // Copy "%" + everything until end‐of‐line + while (i < input.length && input[i] !== "\n") { + out += input[i++]; + } + // Copy the newline too (if any) + if (i < input.length && input[i] === "\n") { + out += "\n"; + i++; + } + inLineComment = false; + continue; + } + + // + // 2) Block comment start "/* … */" + // + if (!inString && !inLineComment && !inBlockComment && ch === "/" && next === "*") { + inBlockComment = true; + out += "/*"; + i += 2; + // Copy until matching "*/" + while (i < input.length) { + if (input[i] === "*" && input[i + 1] === "/") { + out += "*/"; + i += 2; + inBlockComment = false; + break; + } else { + out += input[i++]; + } + } + continue; + } + + // + // 3) If already inside a block comment, copy verbatim until it ends + // + if (inBlockComment) { + out += ch; + i++; + continue; + } + + // + // 4) Toggle inString on unescaped ' or " + // + if (!inLineComment && (ch === "'" || ch === '"') && input[i - 1] !== "\\") { + if (!inString) { + inString = true; + strChar = ch; + out += ch; + i++; + continue; + } else if (inString && ch === strChar) { + inString = false; + strChar = ""; + out += ch; + i++; + continue; + } + } + if (inString) { + // Inside a string → copy verbatim + out += ch; + i++; + continue; + } + + // + // 5) Handle TPTP declaration detection and comma counting + // + if (isAtTPTPStart(i)) { + // If we just ended a formula and are starting a new one, ensure blank line + if (justEndedFormula && !hasBlankLineAtEnd()) { + out += "\n"; + } + justEndedFormula = false; + + const declLength = getTPTPDeclLength(i); + out += input.substring(i, i + declLength); // e.g., "fof(" + i += declLength; + + tptpCommaCount = 0; + isInTPTPFormula = false; + parenDepth = 1; + indentLevel = 1; + + // Parse and keep first two arguments (name, role) inline + let arg = ""; + let commasSeen = 0; + + while (i < input.length && commasSeen < 2) { + const ch2 = input[i]; + + if (ch2 === ",") { + out += arg.trim() + ", "; + arg = ""; + commasSeen++; + i++; + } else { + arg += ch2; + i++; + } + } + + // After second comma, break to a new line and indent for the formula + out += "\n" + indentUnit.repeat(indentLevel); + isInTPTPFormula = true; + + continue; + } + + + // + // 6) Handle "=>" (implication): break‐before, indent at current level, then print "=>", then a space + // + if (ch === "=" && next === ">") { + // newline + indent + out += "\n" + indentUnit.repeat(Math.max(1, indentLevel - 3)) + " =>"; + i += 2; + // skip any whitespace that follows + while (i < input.length && /\s/.test(input[i])) { + i++; + } + out += " "; + continue; + } + + // + // 7) Handle disjunction "|": break‐before, indent one deeper than current level, then "| " + // + if (ch === "|") { + out += "\n" + indentUnit.repeat(Math.max(1, indentLevel - 3)) + "|"; + i++; + // skip following whitespace + while (i < input.length && /\s/.test(input[i])) { + i++; + } + out += " "; + continue; + } + + // 7.1) Handle conjunction "&": break‐before, indent one deeper than current level, then "& " + if (ch === "&") { + out += "\n" + indentUnit.repeat(Math.max(1, indentLevel - 3)) + "&"; + i++; + // skip any whitespace that follows + while (i < input.length && /\s/.test(input[i])) { + i++; + } + out += " "; + continue; + } + + // 7.2) Handle conjunction ":": keep ":" on current line, then newline + indent + if (ch === ":") { + out += " :"; + i++; + // skip any whitespace that follows + while (i < input.length && /\s/.test(input[i])) { + i++; + } + out += "\n" + indentUnit.repeat(Math.max(1, indentLevel - 3)); + continue; + } + + // 7.3) Handle quantifiers ?[ ... ], ![ ... ], ^[ ... ] + if ((ch === "?" || ch === "!" || ch === "^" || ch === "~") && peekNonWhitespace(i + 1) === "[") { + out += ch + " "; + i++; + + // skip any whitespace between quantifier and bracket + while (i < input.length && /\s/.test(input[i])) { + i++; + } + + if (input[i] === "[") { + out += "["; + bracketDepth++; + i++; + continue; + } + } + + // 7.4) Add spaces before special symbols + if ( + (ch === "=" && input[i - 1] !== "<" && input[i - 1] !== "!" && input[i - 1] !== ">") || + (ch === "!" && next === "=") || + (ch === "<" && next === "=") || + (ch === ">" && next === "=") + ) { + const op = (ch === "!" || ch === "<" || ch === ">") ? ch + next : ch; + out += " " + op + " "; + i += op.length; + continue; + } + + // + // 8) Opening parenthesis "(": increase parenDepth & indentLevel, print "(" + // Then, if the next real (non‐whitespace) character is a letter or "!", insert a single space. + // + if (ch === "(") { + out += "("; + parenDepth++; + // indentLevel++; + i++; + + // Peek the next non‐ws character; if it's a letter or "!", insert exactly one space: + const nn = peekNonWhitespace(i); + if (nn !== null && /[A-Za-z!]/.test(nn)) { + // out += " "; + } + continue; + } + + //~ DONT WANT THIS FOR NOW + // 9) Closing parenthesis ")": break‐before at (level−1), then print ")" + // if (ch === ")") { + // let closeCount = 0; + // // Count consecutive closing parens + // while (input[i + closeCount] === ")") { + // closeCount++; + // } + + // // If followed by a period, group them all together + // const followsPeriod = input[i + closeCount] === "."; + + // // Write the closing parens on the same line + // out += " ".repeat(1); // optional space before + // for (let j = 0; j < closeCount; j++) { + // parenDepth = Math.max(parenDepth - 1, 0); + // indentLevel = Math.max(indentLevel - 1, 0); + // out += ")"; + // } + + // i += closeCount; + + // // If there's a period, append it too + // if (followsPeriod) { + // out += ".\n"; + // i++; // skip '.' + // isInTPTPFormula = false; + // tptpCommaCount = 0; + // } + + // continue; + // } + + + // + // 10) Comma ",": + // • Track TPTP comma count and handle formula formatting + // • if parenDepth === 1 → this is the top‐level comma inside "tptp( name, role, formula )": emit "," + newline + indent(at same level) + // • else (nested comma) → emit ", " (comma + single space) on the same line + // + if (ch === ",") { + if (parenDepth === 1 && bracketDepth === 0) { + // top‐level comma in "tptp(...)" + tptpCommaCount++; + out += ","; + + // If this is the second comma (before formula), check line length + if (tptpCommaCount === 2) { + const currentLineLength = getCurrentLineLength(); + if (currentLineLength > maxLineLength) { + out += "\n" + indentUnit.repeat(indentLevel); + isInTPTPFormula = true; + } else { + out += "\n" + indentUnit.repeat(indentLevel); + isInTPTPFormula = true; + } + } else { + out += "\n" + indentUnit.repeat(indentLevel); + } + i++; + } else { + // nested comma, keep on same line + out += ", "; + i++; + // skip any whitespace that follows + while (i < input.length && /\s/.test(input[i])) { + i++; + } + } + continue; + } + + // + // 11) Period "." → print "." then newline, reset TPTP state + // + if (ch === ".") { + out += "."; + out += "\n"; + isInTPTPFormula = false; + tptpCommaCount = 0; + justEndedFormula = true; // Mark that we just ended a formula + i++; + continue; + } + + // + // 12) Whitespace (spaces, tabs, newlines): + // Handle empty line preservation and normal whitespace collapse + // + if (/\s/.test(ch)) { + // Check for multiple consecutive newlines to preserve empty lines + if (ch === '\n') { + const preservedIdx = preserveEmptyLines(i); + if (preservedIdx > i + 1) { + // We preserved multiple newlines, skip ahead + i = preservedIdx; + continue; + } + } + + // Skip all remaining whitespace in input + while (i < input.length && /\s/.test(input[i])) { + i++; + } + + // Now decide whether to insert exactly one space: + const lastCh = out.length > 0 ? out[out.length - 1] : "\n"; + if ( + lastCh !== " " && + lastCh !== "\n" && + lastCh !== "(" + ) { + // Insert one space if the next real char is alphanumeric or "$" or "<" etc. + const nn = peekNonWhitespace(i); + if (nn !== null && /[A-Za-z0-9\$<]/.test(nn)) { + out += " "; + } + } + continue; + } + + // + // 13) Default: any other character—just copy verbatim + // + out += ch; + i++; + } + + // Trim trailing whitespace/newlines, then append exactly one newline at end + return out.replace(/\s*$/, "") + "\n"; +} diff --git a/tptplus/server/src/server.ts b/tptplus/server/src/server.ts index ba9ddcf..d9f32f2 100644 --- a/tptplus/server/src/server.ts +++ b/tptplus/server/src/server.ts @@ -12,10 +12,6 @@ import { TextDocumentPositionParams, TextDocumentSyncKind, InitializeResult, - DocumentFormattingParams, - TextEdit, - Range, - Position, } from 'vscode-languageserver/node'; import { @@ -50,9 +46,7 @@ connection.onInitialize((params: InitializeParams) => { textDocumentSync: TextDocumentSyncKind.Incremental, completionProvider: { resolveProvider: true - }, - documentFormattingProvider: true, - documentRangeFormattingProvider: true, + } } }; if (hasWorkspaceFolderCapability) { @@ -521,498 +515,6 @@ connection.onCompletionResolve( } ); -function prettyPrintTPTP(input: string): string { - const indentUnit = " "; // 4 spaces - const maxLineLength = 20; // threshold for breaking formula to new line - let indentLevel = 0; - let parenDepth = 0; // actual ( ... ) depth - let out = ""; - let inString = false; // tracking '...' or "..." - let strChar = ""; // either "'" or '"' - let inLineComment = false; - let inBlockComment = false; - let isInTPTPFormula = false; // track if we're in the formula part of TPTP declaration - let tptpCommaCount = 0; // count commas in TPTP declaration to identify formula part - let bracketDepth = 0; - let justEndedFormula = false; // track if we just ended a formula with a period - - // Helper: peek ahead, skipping any whitespace - function peekNonWhitespace(idx: number): string | null { - let j = idx; - while (j < input.length && /\s/.test(input[j])) { j++; } - return j < input.length ? input[j] : null; - } - - // Helper: check if current position is start of TPTP declaration - function isAtTPTPStart(idx: number): boolean { - const patterns = ["tpi(", "thf(", "tff(", "tcf(", "fof(", "cnf("]; - return patterns.some(pattern => input.substring(idx, idx + pattern.length) === pattern); - } - - // Helper: get the length of the TPTP declaration type - function getTPTPDeclLength(idx: number): number { - const patterns = ["tpi(", "thf(", "tff(", "tcf(", "fof(", "cnf("]; - for (const pattern of patterns) { - if (input.substring(idx, idx + pattern.length) === pattern) { - return pattern.length; - } - } - return 0; - } - - // Helper: estimate current line length from last newline - function getCurrentLineLength(): number { - const lastNewlineIdx = out.lastIndexOf('\n'); - if (lastNewlineIdx === -1) return out.length; - return out.length - lastNewlineIdx - 1; - } - - // Helper: check if there's already a blank line at the end of output - function hasBlankLineAtEnd(): boolean { - const lines = out.split('\n'); - return lines.length >= 2 && lines[lines.length - 1] === '' && lines[lines.length - 2] === ''; - } - - // Preserve empty lines by tracking consecutive newlines - function preserveEmptyLines(startIdx: number): number { - let i = startIdx; - let newlineCount = 0; - - // Count newlines (but skip other whitespace) - while (i < input.length) { - if (input[i] === '\n') { - newlineCount++; - i++; - } else if (/[ \t\r]/.test(input[i])) { - // Skip other whitespace but don't count it - i++; - } else { - break; - } - } - - // If we have more than one newline, preserve the extras as empty lines - if (newlineCount > 1) { - // Add the extra newlines (newlineCount - 1 because we already have one) - for (let j = 1; j < newlineCount && j < 3; j++) { - out += '\n'; - } - } - - return i; - } - - // We iterate char by char, but sometimes lookahead ("=>" etc.) - for (let i = 0; i < input.length; ) { - const ch = input[i]; - const next = input[i + 1] ?? ""; - - if (ch === "[") { - bracketDepth++; - out += ch; - i++; - continue; - } - - if (ch === "]") { - bracketDepth = Math.max(bracketDepth - 1, 0); - out += ch; - i++; - continue; - } - - // - // 1) Single‐line comment "% …" (only if it occurs at line‐start or after a newline) - // - if ( - !inString && - !inBlockComment && - ch === "%" && - (i === 0 || input[i - 1] === "\n") - ) { - inLineComment = true; - // Copy "%" + everything until end‐of‐line - while (i < input.length && input[i] !== "\n") { - out += input[i++]; - } - // Copy the newline too (if any) - if (i < input.length && input[i] === "\n") { - out += "\n"; - i++; - } - inLineComment = false; - continue; - } - - // - // 2) Block comment start "/* … */" - // - if (!inString && !inLineComment && !inBlockComment && ch === "/" && next === "*") { - inBlockComment = true; - out += "/*"; - i += 2; - // Copy until matching "*/" - while (i < input.length) { - if (input[i] === "*" && input[i + 1] === "/") { - out += "*/"; - i += 2; - inBlockComment = false; - break; - } else { - out += input[i++]; - } - } - continue; - } - - // - // 3) If already inside a block comment, copy verbatim until it ends - // - if (inBlockComment) { - out += ch; - i++; - continue; - } - - // - // 4) Toggle inString on unescaped ' or " - // - if (!inLineComment && (ch === "'" || ch === '"') && input[i - 1] !== "\\") { - if (!inString) { - inString = true; - strChar = ch; - out += ch; - i++; - continue; - } else if (inString && ch === strChar) { - inString = false; - strChar = ""; - out += ch; - i++; - continue; - } - } - if (inString) { - // Inside a string → copy verbatim - out += ch; - i++; - continue; - } - - // - // 5) Handle TPTP declaration detection and comma counting - // - if (isAtTPTPStart(i)) { - // If we just ended a formula and are starting a new one, ensure blank line - if (justEndedFormula && !hasBlankLineAtEnd()) { - out += "\n"; - } - justEndedFormula = false; - - const declLength = getTPTPDeclLength(i); - out += input.substring(i, i + declLength); // e.g., "fof(" - i += declLength; - - tptpCommaCount = 0; - isInTPTPFormula = false; - parenDepth = 1; - indentLevel = 1; - - // Parse and keep first two arguments (name, role) inline - let arg = ""; - let commasSeen = 0; - - while (i < input.length && commasSeen < 2) { - const ch2 = input[i]; - - if (ch2 === ",") { - out += arg.trim() + ", "; - arg = ""; - commasSeen++; - i++; - } else { - arg += ch2; - i++; - } - } - - // After second comma, break to a new line and indent for the formula - out += "\n" + indentUnit.repeat(indentLevel); - isInTPTPFormula = true; - - continue; - } - - - // - // 6) Handle "=>" (implication): break‐before, indent at current level, then print "=>", then a space - // - if (ch === "=" && next === ">") { - // newline + indent - out += "\n" + indentUnit.repeat(Math.max(1, indentLevel - 3)) + " =>"; - i += 2; - // skip any whitespace that follows - while (i < input.length && /\s/.test(input[i])) { - i++; - } - out += " "; - continue; - } - - // - // 7) Handle disjunction "|": break‐before, indent one deeper than current level, then "| " - // - if (ch === "|") { - out += "\n" + indentUnit.repeat(Math.max(1, indentLevel - 3)) + "|"; - i++; - // skip following whitespace - while (i < input.length && /\s/.test(input[i])) { - i++; - } - out += " "; - continue; - } - - // 7.1) Handle conjunction "&": break‐before, indent one deeper than current level, then "& " - if (ch === "&") { - out += "\n" + indentUnit.repeat(Math.max(1, indentLevel - 3)) + "&"; - i++; - // skip any whitespace that follows - while (i < input.length && /\s/.test(input[i])) { - i++; - } - out += " "; - continue; - } - - // 7.2) Handle conjunction ":": keep ":" on current line, then newline + indent - if (ch === ":") { - out += " :"; - i++; - // skip any whitespace that follows - while (i < input.length && /\s/.test(input[i])) { - i++; - } - out += "\n" + indentUnit.repeat(Math.max(1, indentLevel - 3)); - continue; - } - - // 7.3) Handle quantifiers ?[ ... ], ![ ... ], ^[ ... ] - if ((ch === "?" || ch === "!" || ch === "^" || ch === "~") && peekNonWhitespace(i + 1) === "[") { - out += ch + " "; - i++; - - // skip any whitespace between quantifier and bracket - while (i < input.length && /\s/.test(input[i])) { - i++; - } - - if (input[i] === "[") { - out += "["; - bracketDepth++; - i++; - continue; - } - } - - // 7.4) Add spaces before special symbols - if ( - (ch === "=" && input[i - 1] !== "<" && input[i - 1] !== "!" && input[i - 1] !== ">") || - (ch === "!" && next === "=") || - (ch === "<" && next === "=") || - (ch === ">" && next === "=") - ) { - const op = (ch === "!" || ch === "<" || ch === ">") ? ch + next : ch; - out += " " + op + " "; - i += op.length; - continue; - } - - // - // 8) Opening parenthesis "(": increase parenDepth & indentLevel, print "(" - // Then, if the next real (non‐whitespace) character is a letter or "!", insert a single space. - // - if (ch === "(") { - out += "("; - parenDepth++; - // indentLevel++; - i++; - - // Peek the next non‐ws character; if it's a letter or "!", insert exactly one space: - const nn = peekNonWhitespace(i); - if (nn !== null && /[A-Za-z!]/.test(nn)) { - // out += " "; - } - continue; - } - - //~ DONT WANT THIS FOR NOW - // 9) Closing parenthesis ")": break‐before at (level−1), then print ")" - // if (ch === ")") { - // let closeCount = 0; - // // Count consecutive closing parens - // while (input[i + closeCount] === ")") { - // closeCount++; - // } - - // // If followed by a period, group them all together - // const followsPeriod = input[i + closeCount] === "."; - - // // Write the closing parens on the same line - // out += " ".repeat(1); // optional space before - // for (let j = 0; j < closeCount; j++) { - // parenDepth = Math.max(parenDepth - 1, 0); - // indentLevel = Math.max(indentLevel - 1, 0); - // out += ")"; - // } - - // i += closeCount; - - // // If there's a period, append it too - // if (followsPeriod) { - // out += ".\n"; - // i++; // skip '.' - // isInTPTPFormula = false; - // tptpCommaCount = 0; - // } - - // continue; - // } - - - // - // 10) Comma ",": - // • Track TPTP comma count and handle formula formatting - // • if parenDepth === 1 → this is the top‐level comma inside "tptp( name, role, formula )": emit "," + newline + indent(at same level) - // • else (nested comma) → emit ", " (comma + single space) on the same line - // - if (ch === ",") { - if (parenDepth === 1 && bracketDepth === 0) { - // top‐level comma in "tptp(...)" - tptpCommaCount++; - out += ","; - - // If this is the second comma (before formula), check line length - if (tptpCommaCount === 2) { - const currentLineLength = getCurrentLineLength(); - if (currentLineLength > maxLineLength) { - out += "\n" + indentUnit.repeat(indentLevel); - isInTPTPFormula = true; - } else { - out += "\n" + indentUnit.repeat(indentLevel); - isInTPTPFormula = true; - } - } else { - out += "\n" + indentUnit.repeat(indentLevel); - } - i++; - } else { - // nested comma, keep on same line - out += ", "; - i++; - // skip any whitespace that follows - while (i < input.length && /\s/.test(input[i])) { - i++; - } - } - continue; - } - - // - // 11) Period "." → print "." then newline, reset TPTP state - // - if (ch === ".") { - out += "."; - out += "\n"; - isInTPTPFormula = false; - tptpCommaCount = 0; - justEndedFormula = true; // Mark that we just ended a formula - i++; - continue; - } - - // - // 12) Whitespace (spaces, tabs, newlines): - // Handle empty line preservation and normal whitespace collapse - // - if (/\s/.test(ch)) { - // Check for multiple consecutive newlines to preserve empty lines - if (ch === '\n') { - const preservedIdx = preserveEmptyLines(i); - if (preservedIdx > i + 1) { - // We preserved multiple newlines, skip ahead - i = preservedIdx; - continue; - } - } - - // Skip all remaining whitespace in input - while (i < input.length && /\s/.test(input[i])) { - i++; - } - - // Now decide whether to insert exactly one space: - const lastCh = out.length > 0 ? out[out.length - 1] : "\n"; - if ( - lastCh !== " " && - lastCh !== "\n" && - lastCh !== "(" - ) { - // Insert one space if the next real char is alphanumeric or "$" or "<" etc. - const nn = peekNonWhitespace(i); - if (nn !== null && /[A-Za-z0-9\$<]/.test(nn)) { - out += " "; - } - } - continue; - } - - // - // 13) Default: any other character—just copy verbatim - // - out += ch; - i++; - } - - // Trim trailing whitespace/newlines, then append exactly one newline at end - return out.replace(/\s*$/, "") + "\n"; -} - -connection.onDocumentFormatting((params: DocumentFormattingParams): TextEdit[] => { - const uri = params.textDocument.uri; - const doc = documents.get(uri); - if (!doc) { - return []; - } - const fullText = doc.getText(); - const formatted = prettyPrintTPTP(fullText); - - // Replace the entire document - const lastLine = doc.lineCount - 1; - const lastChar = doc.getText({ - start: { line: lastLine, character: 0 }, - end: { line: lastLine + 1, character: 0 }, - }).length; - const fullRange: Range = { - start: Position.create(0, 0), - end: Position.create(lastLine, lastChar), - }; - - return [TextEdit.replace(fullRange, formatted)]; -}); - -// -// (Optional) Range-only formatting if you want to format a selected region -// -connection.onDocumentRangeFormatting((params, _token) => { - const doc = documents.get(params.textDocument.uri); - if (!doc) return []; - const textRange = doc.getText(params.range); - const formattedRangeText = prettyPrintTPTP(textRange); - return [TextEdit.replace(params.range, formattedRangeText)]; -}); - - // Make the text document manager listen on the connection documents.listen(connection);