Use standard LSP requests.

client/src/fstarExtensions.ts

@@ -0,0 +1 @@
+../../server/src/fstarExtensions.ts

server/src/fstar.ts

@@ -1,5 +1,6 @@
 import {
 	WorkspaceFolder,
+	_Connection,
 } from 'vscode-languageserver/node';
 
 import {
@@ -14,7 +15,6 @@ import * as path from 'path';
 import * as util from 'util';
 
 import { fstarVSCodeAssistantSettings } from './settings';
-import { ClientConnection } from './client_connection';
 import { checkFileInDirectory, findFilesByExtension, getEnclosingDirectories } from './utils';
 
 // FStar executable
@@ -85,7 +85,7 @@ export class FStar {
 
 	// Dynamically loads the FStarConfiguration for a given file `textDocument`
 	// before attempting to launch an instance of F*.
-	static async fromInferredConfig(filePath: string, workspaceFolders: WorkspaceFolder[], connection: ClientConnection,
+	static async fromInferredConfig(filePath: string, workspaceFolders: WorkspaceFolder[], connection: _Connection,
 			configurationSettings: fstarVSCodeAssistantSettings, lax?: 'lax'): Promise<FStar | undefined> {
 		const config = await this.getFStarConfig(filePath, workspaceFolders, connection, configurationSettings);
 		return this.trySpawnFstar(config, filePath, configurationSettings.debug, lax);
@@ -105,7 +105,7 @@ export class FStar {
 		});
 	}
 
-	static async parseConfigFile(filePath: string, configFile: string, connection: ClientConnection, configurationSettings: fstarVSCodeAssistantSettings): Promise<FStarConfig> {
+	static async parseConfigFile(filePath: string, configFile: string, connection: _Connection, configurationSettings: fstarVSCodeAssistantSettings): Promise<FStarConfig> {
 		const contents = await util.promisify(fs.readFile)(configFile, 'utf8');
 		function substituteEnvVars(value: string) {
 			return value.replace(/\$([A-Z_]+[A-Z0-9_]*)|\${([A-Z0-9_]*)}/ig,
@@ -115,7 +115,8 @@ export class FStar {
 						return resolved_env_var;
 					}
 					else {
-						connection.sendAlert({ message: "Failed to resolve environment variable " + (a || b), uri: URI.file(filePath).toString() });
+						connection.window.showErrorMessage(
+							`Failed to resolve environment variable ${a || b} for file ${filePath}`);
 						return "";
 					}
 				});
@@ -206,7 +207,7 @@ export class FStar {
 	// 1. An *.fst.config.json file in a parent directory inside the current workspace
 	// 2. The output printed by `make My.File.fst-in`
 	// 3. A default configuration
-	static async getFStarConfig(filePath: string, workspaceFolders: WorkspaceFolder[], connection: ClientConnection, configurationSettings: fstarVSCodeAssistantSettings): Promise<FStarConfig> {
+	static async getFStarConfig(filePath: string, workspaceFolders: WorkspaceFolder[], connection: _Connection, configurationSettings: fstarVSCodeAssistantSettings): Promise<FStarConfig> {
 		// 1. Config file
 		const configFilepath = await this.findConfigFile(filePath, workspaceFolders, configurationSettings);
 		if (configFilepath) {

server/src/fstarExtensions.ts

@@ -0,0 +1,48 @@
+import { ProtocolNotificationType, Position, Range } from 'vscode-languageserver-protocol';
+
+export type StatusKind
+	= 'ok'
+	| 'lax-ok'
+	| 'light-ok'
+	| 'in-progress'
+	| 'failed'
+	| 'light-failed'
+	| 'started';
+
+export interface FragmentStatus {
+	kind: StatusKind;
+	range: Range;
+}
+
+export interface StatusNotificationParams {
+	uri: string;
+	fragments: FragmentStatus[];
+}
+export const statusNotification: ProtocolNotificationType<StatusNotificationParams, RegistrationParams> =
+	new ProtocolNotificationType('$/fstar/status');
+
+export interface RestartParams {
+	uri: string;
+}
+export const restartNotification: ProtocolNotificationType<RestartParams, RegistrationParams> =
+	new ProtocolNotificationType('$/fstar/restart');
+
+export interface KillAndRestartSolverParams {
+	uri: string;
+}
+export const killAndRestartSolverNotification: ProtocolNotificationType<KillAndRestartSolverParams, RegistrationParams> =
+	new ProtocolNotificationType('$/fstar/killAndRestartSolver');
+
+export interface KillAllParams {}
+export const killAllNotification: ProtocolNotificationType<KillAllParams, RegistrationParams> =
+	new ProtocolNotificationType('$/fstar/killAll');
+
+export interface VerifyToPositionParams {
+	uri: string;
+	position: Position;
+	lax: boolean;
+}
+export const verifyToPositionNotification: ProtocolNotificationType<VerifyToPositionParams, RegistrationParams> =
+	new ProtocolNotificationType('$/fstar/verifyToPosition');
+
+interface RegistrationParams {}

server/src/main.ts

@@ -3,21 +3,22 @@
  * Licensed under the MIT License. See License.txt in the project root for license information.
  * ------------------------------------------------------------------------------------------ */
 import {
-	TextDocuments
+	ProposedFeatures,
+	TextDocuments,
+	createConnection,
 } from 'vscode-languageserver/node';
 
 import {
 	TextDocument
 } from 'vscode-languageserver-textdocument';
 
-import { ClientConnection } from './client_connection';
 import { Server } from './server';
 
 // Make unhandled rejections non-fatal
 process.on('unhandledRejection', error => console.log('Unhandled rejection:', error));
 
 // Connection between the LSP server and client (e.g. the extension)
-const connection = new ClientConnection();
+const connection = createConnection(ProposedFeatures.all);
 // Simple text document manager.
 const documents = new TextDocuments(TextDocument);