feat: error handling for pretty-printer (local and remote); detect duplicate formula names

README.md

@@ -158,8 +158,16 @@ Fixed issue where some greater-than-signs are not handled correctly by command "
 
 ### 0.1.9
 
-Added local pretty printer so that "Format TPTP File" works without Internet connection.
-The original remote pretty printer is kept as a fallback.
+Added local pretty-printer so that "Format TPTP File" works without Internet connection.
+The original remote pretty-printer is kept as a fallback.
+
+### 0.1.10
+
+Added error handling for "Format TPTP File": display error message and jump to position of syntax error.
+
+### 0.1.11
+
+Added title-menu button for "TPTP: Check Syntax and Format TPTP File"; improved error handling for pretty-printer.
 
 ---
 

tptplus/CHANGELOG.md

@@ -21,4 +21,6 @@
 - v0.1.5 Added dynamic loading of ATP systems from tptp.org by using fetch.
 - v0.1.7 Automated linting, and standardized releases with GitHub actions.
 - v0.1.8 Fixed issue where some greater-than-signs are not handled correctly by command "Format TPTP File".
-- v0.1.9 Added local pretty printer so that "Format TPTP File" works without Internet connection. The original remote pretty printer is kept as a fallback.
+- v0.1.9 Added local pretty-printer so that "Format TPTP File" works without Internet connection. The original remote pretty-printer is kept as a fallback.
+- v0.1.10 Added error handling for "Format TPTP File": display error message and jump to position of syntax error.
+- v0.1.11 Added title-menu button for "TPTP: Check Syntax and Format TPTP File"; improved error handling for pretty-printer.

tptplus/README.md

@@ -157,8 +157,16 @@ Fixed issue where some greater-than-signs are not handled correctly by command "
 
 ### 0.1.9
 
-Added local pretty printer so that "Format TPTP File" works without Internet connection.
-The original remote pretty printer is kept as a fallback.
+Added local pretty-printer so that "Format TPTP File" works without Internet connection.
+The original remote pretty-printer is kept as a fallback.
+
+### 0.1.10
+
+Added error handling for "Format TPTP File": display error message and jump to position of syntax error.
+
+### 0.1.11
+
+Added title-menu button for "TPTP: Check Syntax and Format TPTP File"; improved error handling for pretty-printer.
 
 ---
 

tptplus/client/resources/wasm/tptp4X_wasm.d.ts

@@ -1,3 +1,3 @@
-declare const createTPTP4X: import('../../src/localPrettyPrinterProcess').CreateTPTP4X;
+declare const createTPTP4X: import('../../src/prettyPrint/localPrettyPrintProcess').CreateTPTP4X;
 
 export = createTPTP4X;

tptplus/client/src/extension.ts

@@ -11,14 +11,19 @@ import {
   TransportKind
 } from 'vscode-languageclient/node';
 
-import {
-  createSystemB4TptpForm
-} from './systemTptpForms';
-import { formatTptpLocally } from './localPrettyPrinter';
+import { createSystemB4TptpForm } from './systemTptpForms';
+import { registerPrettyPrintCommand } from './prettyPrint/prettyPrintCommand';
 
 let client: LanguageClient;
 
 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, {
@@ -314,61 +319,14 @@ export function activate(context: ExtensionContext) {
 
       }
     })
-  })
+  });
 
   context.subscriptions.push(prepareProblem);
 
-  //@ FORMAT A PROBLEM THROUGH SYSTEMB4TPTP
-  const formatProblem = vscode.commands.registerCommand('tptp.formatProblem', async (uri: vscode.Uri) => {
-    if (!uri) {
-      const activeEditor = vscode.window.activeTextEditor;
-      if (!activeEditor) {
-        vscode.window.showErrorMessage('No active TPTP file open');
-        return;
-      }
-      uri = activeEditor.document.uri;
-    }
-
-    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();
-
-    const localOutput =
-      !sourceText.trim() ? "" :  // a whitespace-only file should become empty
-      await formatTptpLocally(context, sourceText);
-    if (localOutput !== undefined) {
-      edit.replace(uri, fullTextRange, localOutput);
-      await vscode.workspace.applyEdit(edit);
-      return;
-    }
-
-    // fall back to remote pretty-printer if the local pretty-printer fails
-    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 match = text.match(/<pre[^>]*>([\s\S]*?)<\/pre>/i);
-
-    let output = sourceText;
-
-    if (match) {  
-      output = match[1].split("\n").slice(2, match[1].split("\n").length - 4).join("\n")
-    }
-
-    edit.replace(uri, fullTextRange, output.replace(/&gt;/g, ">"));
-    await vscode.workspace.applyEdit(edit);
-
-  })
-
-  context.subscriptions.push(formatProblem);
+  //@ FORMAT A PROBLEM BY RUNNING JJPARSER LOCALLY, USING REMOTE SYSTEMB4TPTP AS FALLBACK
+  context.subscriptions.push(
+    registerPrettyPrintCommand(context, prettyPrintDiagnostics)
+  );
 
   //@ RUN A THEOREM THROUGH SYSTEMONTPTP                                              
   const proveProblem = vscode.commands.registerCommand('tptp.proveProblem', async (uri: vscode.Uri) => {
@@ -1663,7 +1621,7 @@ export function activate(context: ExtensionContext) {
       }
     });
 
-  })
+  });
 
   context.subscriptions.push(proveProblemMultiple);
 
@@ -2000,7 +1958,7 @@ export function activate(context: ExtensionContext) {
         }
       }
     })
-  })
+  });
 
   context.subscriptions.push(processSolution);
 
@@ -2341,7 +2299,7 @@ export function activate(context: ExtensionContext) {
         }
       }
     })
-  })
+  });
 
   context.subscriptions.push(processSolutionMultiple);
 
@@ -2387,7 +2345,7 @@ export function activate(context: ExtensionContext) {
     } else {
       vscode.window.showInformationMessage('No problem selected.');
     }
-  })
+  });
 
   context.subscriptions.push(importProblem);
 
@@ -2434,7 +2392,7 @@ export function activate(context: ExtensionContext) {
       vscode.window.showInformationMessage('No Solution selected.');
     }
 
-  })
+  });
 
   context.subscriptions.push(importSolution);