Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add tlaplus-formatter support #327

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
95 changes: 95 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,99 @@
.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') {
reject(err);
}
}

let tempInputPath = path.join(context.globalStorageUri.fsPath, md5Hash, moduleName + '.tla');

Check warning on line 213 in src/main.ts

View workflow job for this annotation

GitHub Actions / build (macOS-latest)

Multiple spaces found before 'moduleName'

Check warning on line 213 in src/main.ts

View workflow job for this annotation

GitHub Actions / build (ubuntu-20.04)

Multiple spaces found before 'moduleName'

Check warning on line 213 in src/main.ts

View workflow job for this annotation

GitHub Actions / build (windows-latest)

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

// if this is a real file, use as input the actual file.
// this is needed because SANY needs to parse also the EXTENDed modules...
// TODO: fails if EXTENDS TLAPS.
if(document.uri.scheme === "file") {

Check warning on line 221 in src/main.ts

View workflow job for this annotation

GitHub Actions / build (macOS-latest)

Expected space(s) after "if"

Check warning on line 221 in src/main.ts

View workflow job for this annotation

GitHub Actions / build (macOS-latest)

Strings must use singlequote

Check warning on line 221 in src/main.ts

View workflow job for this annotation

GitHub Actions / build (ubuntu-20.04)

Expected space(s) after "if"

Check warning on line 221 in src/main.ts

View workflow job for this annotation

GitHub Actions / build (ubuntu-20.04)

Strings must use singlequote

Check warning on line 221 in src/main.ts

View workflow job for this annotation

GitHub Actions / build (windows-latest)

Expected space(s) after "if"

Check warning on line 221 in src/main.ts

View workflow job for this annotation

GitHub Actions / build (windows-latest)

Strings must use singlequote
tempInputPath = document.uri.fsPath;
}
// 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', '-v', 'ERROR', tempInputPath, tempInputPath]);

Check warning on line 227 in src/main.ts

View workflow job for this annotation

GitHub Actions / build (macOS-latest)

This line has a length of 185. Maximum allowed is 120

Check warning on line 227 in src/main.ts

View workflow job for this annotation

GitHub Actions / build (ubuntu-20.04)

This line has a length of 185. Maximum allowed is 120

Check warning on line 227 in src/main.ts

View workflow job for this annotation

GitHub Actions / build (windows-latest)

This line has a length of 185. Maximum allowed is 120
// 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)];

Check warning on line 250 in src/main.ts

View workflow job for this annotation

GitHub Actions / build (macOS-latest)

This line has a length of 125. Maximum allowed is 120

Check warning on line 250 in src/main.ts

View workflow job for this annotation

GitHub Actions / build (ubuntu-20.04)

This line has a length of 125. Maximum allowed is 120

Check warning on line 250 in src/main.ts

View workflow job for this annotation

GitHub Actions / build (windows-latest)

This line has a length of 125. Maximum allowed is 120
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
Loading