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/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 b2f7c29..bf1a570 100644
--- a/tptplus/client/src/extension.ts
+++ b/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')
diff --git a/tptplus/client/src/prettyPrint/command.ts b/tptplus/client/src/prettyPrint/command.ts
new file mode 100644
index 0000000..b161692
--- /dev/null
+++ b/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);
+    })
+  );
+}
diff --git a/tptplus/client/src/prettyPrint/jjParserDiagnostics.ts b/tptplus/client/src/prettyPrint/diagnostics.ts
similarity index 63%
rename from tptplus/client/src/prettyPrint/jjParserDiagnostics.ts
rename to tptplus/client/src/prettyPrint/diagnostics.ts
index 189813b..755edda 100644
--- a/tptplus/client/src/prettyPrint/jjParserDiagnostics.ts
+++ b/tptplus/client/src/prettyPrint/diagnostics.ts
@@ -1,37 +1,27 @@
-import * as vscode from "vscode";
+import * as vscode from 'vscode';
+import type { PrettyPrintSourceErrorLocation } from './types';
 
-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<void>
 {
   const position = errorLocation?.position;
diff --git a/tptplus/client/src/prettyPrint/jjParserErrors.ts b/tptplus/client/src/prettyPrint/jjParserErrors.ts
new file mode 100644
index 0000000..41aaa8a
--- /dev/null
+++ b/tptplus/client/src/prettyPrint/jjParserErrors.ts
@@ -0,0 +1,43 @@
+import type { PrettyPrintSourceErrorLocation } from './types';
+
+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/local.ts
similarity index 75%
rename from tptplus/client/src/prettyPrint/localPrettyPrint.ts
rename to tptplus/client/src/prettyPrint/local.ts
index b40cdeb..0a49359 100644
--- a/tptplus/client/src/prettyPrint/localPrettyPrint.ts
+++ b/tptplus/client/src/prettyPrint/local.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 './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
 
-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,15 @@ function readParserError(stderr: string): string | undefined {
 export async function formatTptpLocally(
   context: vscode.ExtensionContext,
   input: string
-): Promise<LocalPrettyPrintResult> {
+): Promise<PrettyPrintFormatterResult> {
 
   // // 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: '' };
+  }
 
   return new Promise(resolve => {
     let stdout = '';
@@ -50,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);
@@ -60,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/localProcess.ts
similarity index 97%
rename from tptplus/client/src/prettyPrint/localPrettyPrintProcess.ts
rename to tptplus/client/src/prettyPrint/localProcess.ts
index ca73108..7096189 100644
--- a/tptplus/client/src/prettyPrint/localPrettyPrintProcess.ts
+++ b/tptplus/client/src/prettyPrint/localProcess.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
deleted file mode 100644
index 7d530dc..0000000
--- a/tptplus/client/src/prettyPrint/prettyPrintCommand.ts
+++ /dev/null
@@ -1,111 +0,0 @@
-import * as vscode from "vscode";
-
-import {
-  getJJParserErrorLocation,
-  revealJJParserErrorLocation,
-  setJJParserErrorDiagnostic
-} from './jjParserDiagnostics';
-import { formatTptpLocally } from './localPrettyPrint';
-import { isDuplicateFormulaNameError } from './prettyPrintErrors';
-import { createSystemB4TptpForm } from '../systemTptpForms';
-import {
-  extractSystemB4TptpOutput,
-  lastNonemptyLine
-} from '../systemB4TptpOutput';
-
-export function registerPrettyPrintCommand(
-  context: vscode.ExtensionContext,
-  prettyPrintDiagnostics: vscode.DiagnosticCollection
-): vscode.Disposable {
-  return vscode.commands.registerCommand('tptp.prettyPrint', async (uri: vscode.Uri) => {
-    if (!uri) {
-      const activeEditor = vscode.window.activeTextEditor;
-      if (!activeEditor) {
-        vscode.window.showErrorMessage('No active TPTP file open');
-        return;
-      }
-      uri = activeEditor.document.uri;
-    }
-
-    // Clear stale parser diagnostics before each new pretty-printer run.
-    prettyPrintDiagnostics.delete(uri);
-
-    const document = await vscode.workspace.openTextDocument(uri);
-    const sourceText = document.getText();
-    const fullTextRange = new vscode.Range(
-      document.positionAt(0),
-      document.positionAt(sourceText.length)
-    );
-
-    // use WorkspaceEdit to edit any URI's document, even if it's invisible
-    const edit = new vscode.WorkspaceEdit();
-
-    // a whitespace-only file should become empty
-    if (!sourceText.trim()) {
-      edit.replace(uri, fullTextRange, '');
-      await vscode.workspace.applyEdit(edit);
-      return;
-    }
-
-    // run the local pretty-printer (JJParser)
-    const localResult = await formatTptpLocally(context, sourceText);
-
-    if (localResult.kind === 'success') {
-      edit.replace(uri, fullTextRange, localResult.output);
-      await vscode.workspace.applyEdit(edit);
-      return;
-    }
-
-    if (localResult.kind === 'parser-error') {
-      if (isDuplicateFormulaNameError(localResult.message)) {
-        vscode.window.showErrorMessage(`Failed to format TPTP file: ${localResult.message}`);
-        return;
-      }
-
-      const errorLocation = getJJParserErrorLocation(document, localResult.message);
-      if (errorLocation !== undefined) {
-        setJJParserErrorDiagnostic(prettyPrintDiagnostics, document, errorLocation);
-        await revealJJParserErrorLocation(document, errorLocation);
-        vscode.window.showErrorMessage(`Failed to format TPTP file: ${localResult.message}`);
-        return;
-      }
-    }
-
-    // Fall back to remote pretty-printer if the local pretty-printer fails on a critical error,
-    // i.e., either an `unknown-error`, or a `parser-error` that is not a duplicate formula name
-    // error and does not point to any specific location in `sourceText`.
-    const localFailMessage =
-      localResult.kind === 'parser-error' ? localResult.message : 'unknown error';
-    vscode.window.showWarningMessage(
-        `Failed to format TPTP file locally: ${localFailMessage}. ` +
-        'Trying the remote formatter provided by SystemB4TPTP...'
-    );
-
-    // run the remote pretty-printer (provided by SystemB4TPTP)
-    const form = createSystemB4TptpForm(sourceText, null);
-    const response = await fetch('https://tptp.org/cgi-bin/SystemOnTPTPFormReply', {
-      method: 'POST',
-      body: form
-    });
-    const text = await response.text();
-    const formattedOutput = extractSystemB4TptpOutput(text);
-
-    if (formattedOutput !== undefined) {
-      const lastLine = lastNonemptyLine(formattedOutput);
-      if (lastLine?.startsWith('ERROR: ')) {
-        const errorLocation = getJJParserErrorLocation(document, lastLine);
-        setJJParserErrorDiagnostic(prettyPrintDiagnostics, document, errorLocation);
-        await revealJJParserErrorLocation(document, errorLocation);
-        vscode.window.showErrorMessage(
-          'Failed to format TPTP file: ' +
-          `remote formatter provided by SystemB4TPTP exited with ${lastLine}`
-        );
-      } else {
-        edit.replace(uri, fullTextRange, formattedOutput);
-        await vscode.workspace.applyEdit(edit);
-        vscode.window.showInformationMessage('Format TPTP file successful.');
-      }
-    }
-
-  });
-}
diff --git a/tptplus/client/src/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/remote.ts b/tptplus/client/src/prettyPrint/remote.ts
new file mode 100644
index 0000000..34c10c1
--- /dev/null
+++ b/tptplus/client/src/prettyPrint/remote.ts
@@ -0,0 +1,42 @@
+import { errorMessage } from '../errorMessage';
+import {
+  extractSystemB4TptpOutput,
+  lastNonemptyLine
+} from '../systemB4TptpOutput';
+import { createSystemB4TptpForm } from '../systemTptpForms';
+import type { PrettyPrintFormatterResult } from './types';
+
+const SYSTEM_ON_TPTP_URL = 'https://tptp.org/cgi-bin/SystemOnTPTPFormReply';
+
+/** Formats TPTP source using the SystemB4TPTP remote pretty-printer. */
+export async function formatTptpRemotely(
+  sourceText: string
+): Promise<PrettyPrintFormatterResult> {
+  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) };
+  }
+}
diff --git a/tptplus/client/src/prettyPrint/state.ts b/tptplus/client/src/prettyPrint/state.ts
new file mode 100644
index 0000000..87bfe68
--- /dev/null
+++ b/tptplus/client/src/prettyPrint/state.ts
@@ -0,0 +1,18 @@
+/**
+ * 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 formattedVersionByDocument = new WeakMap<vscode.TextDocument, number>();
+
+/** 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 successfully formatted. */
+export function markPrettyPrintVersionFormatted(document: vscode.TextDocument): void {
+  formattedVersionByDocument.set(document, document.version);
+}
diff --git a/tptplus/client/src/prettyPrint/types.ts b/tptplus/client/src/prettyPrint/types.ts
new file mode 100644
index 0000000..ff79703
--- /dev/null
+++ b/tptplus/client/src/prettyPrint/types.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<PrettyPrintFormatterResult>;
diff --git a/tptplus/client/src/prettyPrint/workflow.ts b/tptplus/client/src/prettyPrint/workflow.ts
new file mode 100644
index 0000000..f56ac37
--- /dev/null
+++ b/tptplus/client/src/prettyPrint/workflow.ts
@@ -0,0 +1,93 @@
+import { errorMessage } from '../errorMessage';
+import {
+  parseJJParserError,
+  type ParsedJJParserError
+} from './jjParserErrors';
+import type {
+  PrettyPrintFormatter,
+  PrettyPrintFormatterFunction,
+  PrettyPrintFormatterResult,
+  PrettyPrintOutcome
+} from './types';
+
+export interface PrettyPrintWorkflowDependencies {
+  formatLocally: PrettyPrintFormatterFunction;
+  formatRemotely: PrettyPrintFormatterFunction;
+  onRemoteFallback?(localFailureMessage: string): void | Promise<void>;
+}
+
+/** Ensures an adapter exception is represented by the same result type as other failures. */
+async function callFormatter(
+  formatter: PrettyPrintFormatterFunction,
+  sourceText: string
+): Promise<PrettyPrintFormatterResult> {
+  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<PrettyPrintOutcome> {
+  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/package.json b/tptplus/package.json
index 1eb9490..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"
@@ -57,6 +53,7 @@
       {
         "command": "tptp.prettyPrint",
         "title": "TPTP: Pretty-Print TPTP File",
+        "enablement": "!tptp.prettyPrintRunning",
         "icon": {
           "light": "./images/icons/PrettyPrint.png",
           "dark": "./images/icons/PrettyPrint.png"
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);