Add reformatting capability

client/src/VerificationController.ts

@@ -13,7 +13,7 @@ import { URI } from 'vscode-uri';
 import { Location } from 'vs-verification-toolbox';
 import { AwaitTimer } from './AwaitTimer';
 import { State } from './ExtensionState';
-import { Common, VerifyParams, TimingInfo, VerificationState, Commands, StateChangeParams, LogLevel, Success, Backend, StopVerificationRequest } from './ViperProtocol';
+import { Common, VerifyParams, TimingInfo, VerificationState, Commands, StateChangeParams, LogLevel, Success, Backend, StopVerificationRequest, ReformatParams } from './ViperProtocol';
 import { Log } from './Log';
 import { Helper } from './Helper';
 import { ViperFileState } from './ViperFileState';

client/src/ViperProtocol.ts

@@ -50,6 +50,8 @@ export class Commands {
     static GetVersion: RequestType<GetVersionRequest, GetVersionResponse, void> = new RequestType("GetVersion");
     //Client requests verification for a file
     static Verify: NotificationType<VerifyParams> = new NotificationType("Verify");
+    //Client requests reformatting for a file
+    static Reformat: RequestType<ReformatParams, void, string> = new RequestType("Reformat");
     //Client tells server to abort the running verification
     static StopVerification: RequestType<StopVerificationRequest, StopVerificationResponse, void> = new RequestType("StopVerification");
     static GetLanguageServerUrl: RequestType0<GetLanguageServerUrlResponse, void> = new RequestType0("GetLanguageServerUrl");
@@ -97,6 +99,10 @@ export interface VerifyParams {
     customArgs: string;
 }
 
+export interface ReformatParams {
+    uri: string
+}
+
 export interface Command {
     method: string;
 }

client/src/extension.ts

@@ -22,7 +22,7 @@ import * as rimraf from 'rimraf';
 import * as vscode from 'vscode';
 import { URI } from 'vscode-uri';
 import { State } from './ExtensionState';
-import { HintMessage, Commands, StateChangeParams, LogLevel, LogParams, UnhandledViperServerMessageTypeParams, FlushCacheParams, Backend, Position, VerificationNotStartedParams } from './ViperProtocol';
+import { HintMessage, Commands, StateChangeParams, LogLevel, LogParams, UnhandledViperServerMessageTypeParams, FlushCacheParams, Backend, Position, VerificationNotStartedParams, ReformatParams } from './ViperProtocol';
 import { Log } from './Log';
 import { Helper } from './Helper';
 import { locateViperTools } from './ViperTools';
@@ -31,6 +31,7 @@ import { VerificationController, TaskType, Task } from './VerificationController
 import { ViperApi } from './ViperApi';
 import { Settings } from './Settings';
 import { Location } from 'vs-verification-toolbox';
+import { integer } from 'vscode-languageclient';
 
 let fileSystemWatcher: vscode.FileSystemWatcher;
 
@@ -254,6 +255,52 @@ function registerContextHandlers(context: vscode.ExtensionContext, location: Loc
         }
     }));
 
+    // TODO: See the comment in viperserver for why we currently register a custom formatting
+    // provider instead of registering it inside the LSP and letting the LSP protocol take
+    // care of registering the command.
+    context.subscriptions.push(vscode.languages.registerDocumentFormattingEditProvider('viper', {
+        async provideDocumentFormattingEdits(document: vscode.TextDocument): Promise<vscode.TextEdit[]> {
+            if (!State.isReady()) {
+                showNotReadyHint();
+                return;
+            }
+
+            const fileUri = Helper.getActiveFileUri();
+
+            // Need to save document first, otherwise if someone types something real quick and
+            // attempts to reformat, the changes might be lost since the file hasn't been written
+            // to disk yet.
+            const saved = await document.save();
+
+            if (!saved) {
+                Log.log("Failed to reformat file because it couldn't be saved.", LogLevel.Info);
+                return [];
+            }
+
+            if (!fileUri) {
+                Log.log("Cannot reformat, no document is open.", LogLevel.Info);
+            } else if (!Helper.isViperSourceFile(fileUri)) {
+                Log.log("Cannot reformat the active file, it's not a viper file.", LogLevel.Info);
+            } else {
+                Log.log("Attempting to reformat a file...", LogLevel.Info);
+                try {
+                    const params: ReformatParams = { uri: fileUri.toString()};
+                    return State.client.sendRequest(Commands.Reformat, params).then(a => {
+                        if (a["value"]) {
+                            const range = new vscode.Range(document.lineAt(0).range.start, document.lineAt(document.lineCount - 1).range.end);
+                            return [vscode.TextEdit.replace(range, a["value"])];
+                        } else  {
+                            Log.log("Empty result returned when attempting to reformat. Ignoring.", LogLevel.Info);
+                            return [];
+                        }
+                    });
+                } catch (e) { 
+                    Log.error(`Failed to reformat file: ${e.toString()}`);
+                }
+            }
+        }
+    }))
+
     //verifyAllFilesInWorkspace
     context.subscriptions.push(vscode.commands.registerCommand('viper.verifyAllFilesInWorkspace', async (folder: string) => {
         if (!State.isReady()) {