Skip to content

Commit

Permalink
Add tlaplus-formatter support
Browse files Browse the repository at this point in the history
  • Loading branch information
FedericoPonzi committed Jul 21, 2024
1 parent d2e1743 commit 1a5b90d
Showing 1 changed file with 89 additions and 0 deletions.
89 changes: 89 additions & 0 deletions src/main.ts
Original file line number Diff line number Diff line change
@@ -1,5 +1,9 @@
import * as vscode from 'vscode';
import * as path from 'path';
import * as fs from 'fs';
import { createHash } from 'crypto';
import { spawn } from 'child_process';

import {
CMD_CHECK_MODEL_RUN, CMD_CHECK_MODEL_STOP, CMD_CHECK_MODEL_DISPLAY, CMD_SHOW_TLC_OUTPUT,
CMD_CHECK_MODEL_CUSTOM_RUN, checkModel, displayModelChecking, stopModelChecking,
Expand Down Expand Up @@ -185,8 +189,93 @@ export function activate(context: vscode.ExtensionContext): void {
.then(() => listenTlcStatConfigurationChanges(context.subscriptions));
showChangeLog(context.extensionPath)
.catch((err) => console.error(err));

context.subscriptions.push(
vscode.languages.registerDocumentFormattingEditProvider('tlaplus', {
provideDocumentFormattingEdits(document: vscode.TextDocument): vscode.ProviderResult<vscode.TextEdit[]> {
return new Promise((resolve, reject) => {
const inputText = document.getText();
// need the module name to create the file. The filename should match the module name.
const moduleName = extractModuleName(inputText);
// create a unique temp folder.
const md5Hash = generateHash(inputText, 'md5');
const tempDir = path.join(context.globalStorageUri.fsPath, md5Hash);

// create folder if not exists
try {
fs.mkdirSync(tempDir);
} catch (err) {
if ((err as NodeJS.ErrnoException).code !== 'EEXIST') {
throw err;
}
}

const tempInputPath = path.join(context.globalStorageUri.fsPath, md5Hash, moduleName + '.tla');
const tempOutputPath = path.join(context.globalStorageUri.fsPath, md5Hash, moduleName + '.tla');
// Write input text to temporary file
fs.writeFileSync(tempInputPath, inputText);

// Execute the Java formatter

// Execute the Java formatter using spawn
const javaProcess = spawn('java', ['-jar', '/home/fponzi/dev/tla+/tlaplus-formatter/build/libs/tlaplus-formatter.jar', tempInputPath, tempOutputPath]);
// Capture and log standard output
javaProcess.stdout.on('data', (data) => {
console.log(`STDOUT: ${data}`);
});

// Capture and log standard error
javaProcess.stderr.on('data', (data) => {
console.error(`STDERR: ${data}`);
});

javaProcess.on('error', (error) => {
vscode.window.showErrorMessage(`Formatter failed: ${error.message}`);
reject(error);
});

javaProcess.on('close', (code) => {
if (code !== 0) {
vscode.window.showErrorMessage(`Formatter failed with exit code ${code}`);
return reject(new Error(`Formatter failed with exit code ${code}`));
}
// Read the formatted text
const formattedText = fs.readFileSync(tempOutputPath, 'utf8');
const edit = [vscode.TextEdit.replace(new vscode.Range(0, 0, document.lineCount, 0), formattedText)];
fs.rmSync(tempDir, { recursive: true, force: true });
resolve(edit);
});
});
}
})
);

// Register a command to manually trigger formatting
const disposable = vscode.commands.registerCommand('extension.formatDocument', () => {
const editor = vscode.window.activeTextEditor;
if (editor) {
vscode.commands.executeCommand('editor.action.formatDocument');
}
});

context.subscriptions.push(disposable);
}

function generateHash(input: string, algorithm: string): string {
const hash = createHash(algorithm);
hash.update(input);
return hash.digest('hex');
}
function extractModuleName(text: string): string | null {
const regex = /MODULE\s+(\w+)/;
const match = regex.exec(text);
if (match && match[1]) {
return match[1];
}
return null;
}


export function deactivate() {
if (tlapsClient) {
tlapsClient.deactivate();
Expand Down

0 comments on commit 1a5b90d

Please sign in to comment.