feat: improve error handling for pretty-printer; retire legacy server formatting

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;

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);
+}

tptplus/client/src/extension.ts

@@ -11,20 +11,13 @@ import {
   TransportKind
 } from 'vscode-languageclient/node';
 
+import { errorMessage } from './errorMessage';
 import { createSystemB4TptpForm } from './systemTptpForms';
-import { registerPrettyPrintCommand } from './prettyPrint/prettyPrintCommand';
+import { registerPrettyPrintCommand } from './prettyPrint/command';
 
 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 +317,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) => {
@@ -989,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)}`);
         }
       }
     });
@@ -1611,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)}`);
         }
       }
     });
@@ -1949,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)}`);
         }
       }
     })
@@ -2290,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)}`);
         }
       }
     })
@@ -2396,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')

tptplus/client/src/prettyPrint/command.ts

@@ -0,0 +1,210 @@
+import * as vscode from 'vscode';
+
+import { errorMessage } from '../errorMessage';
+import {
+  createJJParserDiagnosticLocation,
+  revealJJParserErrorLocation,
+  setJJParserErrorDiagnostic
+} from './diagnostics';
+import { formatTptpLocally } from './local';
+import { formatTptpWithFallback } from './workflow';
+import { formatTptpRemotely } from './remote';
+import {
+  isPrettyPrintVersionKnownFormatted,
+  markPrettyPrintVersionFormatted
+} from './state';
+import type { PrettyPrintOutcome } from './types';
+
+const PRETTY_PRINT_COMMAND = 'tptp.prettyPrint';
+const PRETTY_PRINT_RUNNING_CONTEXT_KEY = 'tptp.prettyPrintRunning';
+
+async function setPrettyPrintRunningContext(running: boolean): Promise<void> {
+  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,
+  snapshot: DocumentSnapshot,
+  output: string
+): Promise<ApplyPrettyPrintResult> {
+  if (document.version !== snapshot.version) {
+    return 'stale';
+  }
+
+  if (snapshot.text === output) {
+    return 'unchanged';
+  }
+
+  const edit = new vscode.WorkspaceEdit();
+  const fullTextRange = new vscode.Range(
+    document.positionAt(0),
+    document.positionAt(snapshot.text.length)
+  );
+  edit.replace(document.uri, fullTextRange, output);
+
+  return await vscode.workspace.applyEdit(edit) ? 'applied' : 'rejected';
+}
+
+async function reportSourceError(
+  diagnostics: vscode.DiagnosticCollection,
+  document: vscode.TextDocument,
+  outcome: Extract<PrettyPrintOutcome, { kind: 'source-error' }>
+): Promise<void> {
+  const errorLocation = createJJParserDiagnosticLocation(
+    document,
+    outcome.message,
+    outcome.location
+  );
+  setJJParserErrorDiagnostic(diagnostics, document, errorLocation);
+  await revealJJParserErrorLocation(document, errorLocation);
+
+  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);
+}
+
+async function presentPrettyPrintOutcome(
+  diagnostics: vscode.DiagnosticCollection,
+  document: vscode.TextDocument,
+  snapshot: DocumentSnapshot,
+  outcome: PrettyPrintOutcome
+): Promise<void> {
+  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') {
+    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;
+  }
+
+  const applyResult = await applyPrettyPrintResult(document, snapshot, outcome.output);
+  switch (applyResult) {
+    case 'applied':
+      markPrettyPrintVersionFormatted(document);
+      vscode.window.showInformationMessage('TPTP file formatted successfully.');
+      return;
+    case 'unchanged':
+      markPrettyPrintVersionFormatted(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.'
+      );
+  }
+}
+
+async function executePrettyPrint(
+  context: vscode.ExtensionContext,
+  diagnostics: vscode.DiagnosticCollection,
+  uri: vscode.Uri
+): Promise<void> {
+  const document = await vscode.workspace.openTextDocument(uri);
+  if (isPrettyPrintVersionKnownFormatted(document)) {
+    vscode.window.showInformationMessage(
+      'The file has not changed since it was last successfully formatted.'
+    );
+    return;
+  }
+
+  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);
+}
+
+function createPrettyPrintCommandHandler(
+  context: vscode.ExtensionContext,
+  diagnostics: vscode.DiagnosticCollection
+): (uri?: vscode.Uri) => Promise<void> {
+  let prettyPrintRunning = false;
+
+  return async (uri?: vscode.Uri): Promise<void> => {
+    if (prettyPrintRunning) {
+      vscode.window.showInformationMessage('The TPTP pretty-printer is already running.');
+      return;
+    }
+
+    const targetUri = getTargetUri(uri);
+    if (!targetUri) {
+      vscode.window.showErrorMessage('No TPTP file is currently open.');
+      return;
+    }
+
+    prettyPrintRunning = true;
+    try {
+      await setPrettyPrintRunningContext(true);
+      await executePrettyPrint(context, diagnostics, targetUri);
+    } catch (error: unknown) {
+      vscode.window.showErrorMessage(`Failed to format TPTP file: ${errorMessage(error)}`);
+    } finally {
+      await setPrettyPrintRunningContext(false);
+      prettyPrintRunning = false;
+    }
+  };
+}
+
+/** 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(
+    diagnostics,
+    vscode.commands.registerCommand(PRETTY_PRINT_COMMAND, commandHandler),
+    vscode.workspace.onDidChangeTextDocument(event => {
+      diagnostics.delete(event.document.uri);
+    })
+  );
+}