|
1 | 1 | import * as vscode from 'vscode'; |
2 | 2 | import * as path from 'path'; |
| 3 | +import * as fs from 'fs'; |
| 4 | +import { createHash } from 'crypto'; |
| 5 | +import { spawn } from 'child_process'; |
| 6 | + |
3 | 7 | import { |
4 | 8 | CMD_CHECK_MODEL_RUN, CMD_CHECK_MODEL_STOP, CMD_CHECK_MODEL_DISPLAY, CMD_SHOW_TLC_OUTPUT, |
5 | 9 | CMD_CHECK_MODEL_CUSTOM_RUN, checkModel, displayModelChecking, stopModelChecking, |
@@ -185,8 +189,99 @@ export function activate(context: vscode.ExtensionContext): void { |
185 | 189 | .then(() => listenTlcStatConfigurationChanges(context.subscriptions)); |
186 | 190 | showChangeLog(context.extensionPath) |
187 | 191 | .catch((err) => console.error(err)); |
| 192 | + |
| 193 | + context.subscriptions.push( |
| 194 | + vscode.languages.registerDocumentFormattingEditProvider('tlaplus', { |
| 195 | + provideDocumentFormattingEdits(document: vscode.TextDocument): vscode.ProviderResult<vscode.TextEdit[]> { |
| 196 | + return new Promise((resolve, reject) => { |
| 197 | + const inputText = document.getText(); |
| 198 | + // need the module name to create the file. The filename should match the module name. |
| 199 | + const moduleName = extractModuleName(inputText); |
| 200 | + // create a unique temp folder. |
| 201 | + const md5Hash = generateHash(inputText, 'md5'); |
| 202 | + const tempDir = path.join(context.globalStorageUri.fsPath, md5Hash); |
| 203 | + |
| 204 | + // create folder if not exists |
| 205 | + try { |
| 206 | + fs.mkdirSync(tempDir); |
| 207 | + } catch (err) { |
| 208 | + if ((err as NodeJS.ErrnoException).code !== 'EEXIST') { |
| 209 | + reject(err); |
| 210 | + } |
| 211 | + } |
| 212 | + |
| 213 | + let tempInputPath = path.join(context.globalStorageUri.fsPath, md5Hash, moduleName + '.tla'); |
| 214 | + const tempOutputPath = path.join(context.globalStorageUri.fsPath, md5Hash, moduleName + '.tla'); |
| 215 | + // Write input text to temporary file |
| 216 | + fs.writeFileSync(tempInputPath, inputText); |
| 217 | + |
| 218 | + // if this is a real file, use as input the actual file. |
| 219 | + // this is needed because SANY needs to parse also the EXTENDed modules... |
| 220 | + // TODO: fails if EXTENDS TLAPS. |
| 221 | + if(document.uri.scheme === "file") { |
| 222 | + tempInputPath = document.uri.fsPath; |
| 223 | + } |
| 224 | + // Execute the Java formatter |
| 225 | + |
| 226 | + // Execute the Java formatter using spawn |
| 227 | + const javaProcess = spawn('java', ['-jar', '/home/fponzi/dev/tla+/tlaplus-formatter/build/libs/tlaplus-formatter.jar', '-v', 'ERROR', tempInputPath, tempInputPath]); |
| 228 | + // Capture and log standard output |
| 229 | + javaProcess.stdout.on('data', (data) => { |
| 230 | + console.log(`STDOUT: ${data}`); |
| 231 | + }); |
| 232 | + |
| 233 | + // Capture and log standard error |
| 234 | + javaProcess.stderr.on('data', (data) => { |
| 235 | + console.error(`STDERR: ${data}`); |
| 236 | + }); |
| 237 | + |
| 238 | + javaProcess.on('error', (error) => { |
| 239 | + vscode.window.showErrorMessage(`Formatter failed: ${error.message}`); |
| 240 | + reject(error); |
| 241 | + }); |
| 242 | + |
| 243 | + javaProcess.on('close', (code) => { |
| 244 | + if (code !== 0) { |
| 245 | + vscode.window.showErrorMessage(`Formatter failed with exit code ${code}`); |
| 246 | + return reject(new Error(`Formatter failed with exit code ${code}`)); |
| 247 | + } |
| 248 | + // Read the formatted text |
| 249 | + const formattedText = fs.readFileSync(tempOutputPath, 'utf8'); |
| 250 | + const edit = [vscode.TextEdit.replace(new vscode.Range(0, 0, document.lineCount, 0), formattedText)]; |
| 251 | + fs.rmSync(tempDir, { recursive: true, force: true }); |
| 252 | + resolve(edit); |
| 253 | + }); |
| 254 | + }); |
| 255 | + } |
| 256 | + }) |
| 257 | + ); |
| 258 | + |
| 259 | + // Register a command to manually trigger formatting |
| 260 | + const disposable = vscode.commands.registerCommand('extension.formatDocument', () => { |
| 261 | + const editor = vscode.window.activeTextEditor; |
| 262 | + if (editor) { |
| 263 | + vscode.commands.executeCommand('editor.action.formatDocument'); |
| 264 | + } |
| 265 | + }); |
| 266 | + |
| 267 | + context.subscriptions.push(disposable); |
188 | 268 | } |
189 | 269 |
|
| 270 | +function generateHash(input: string, algorithm: string): string { |
| 271 | + const hash = createHash(algorithm); |
| 272 | + hash.update(input); |
| 273 | + return hash.digest('hex'); |
| 274 | +} |
| 275 | +function extractModuleName(text: string): string | null { |
| 276 | + const regex = /MODULE\s+(\w+)/; |
| 277 | + const match = regex.exec(text); |
| 278 | + if (match && match[1]) { |
| 279 | + return match[1]; |
| 280 | + } |
| 281 | + return null; |
| 282 | +} |
| 283 | + |
| 284 | + |
190 | 285 | export function deactivate() { |
191 | 286 | if (tlapsClient) { |
192 | 287 | tlapsClient.deactivate(); |
|
0 commit comments