Use standard LSP requests.

client/src/fstarLspExtensions.ts

@@ -0,0 +1 @@
+../../server/src/fstarLspExtensions.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/fstarLspExtensions.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 =
+	new ProtocolNotificationType<StatusNotificationParams, RegistrationParams>('$/fstar/status');
+
+export interface RestartParams {
+	uri: string;
+}
+export const restartNotification =
+	new ProtocolNotificationType<RestartParams, RegistrationParams>('$/fstar/restart');
+
+export interface KillAndRestartSolverParams {
+	uri: string;
+}
+export const killAndRestartSolverNotification =
+	new ProtocolNotificationType<KillAndRestartSolverParams, RegistrationParams>('$/fstar/killAndRestartSolver');
+
+export interface KillAllParams {}
+export const killAllNotification =
+	new ProtocolNotificationType<KillAllParams, RegistrationParams>('$/fstar/killAll');
+
+export interface VerifyToPositionParams {
+	uri: string;
+	position: Position;
+	lax: boolean;
+}
+export const verifyToPositionNotification =
+	new ProtocolNotificationType<VerifyToPositionParams, RegistrationParams>('$/fstar/verifyToPosition');
+
+interface RegistrationParams {}

server/src/fstar_connection.ts

@@ -37,7 +37,7 @@ export class FStarConnection {
 		bufferedFBR?: FullBufferQuery;
 	};
 
-	onFullBufferResponse: (msg: any) => void = _ => {};
+	onFullBufferResponse: (msg: any, query: FullBufferQuery) => void = _ => {};
 
 	constructor(private fstar: FStar, public debug: boolean) {
 		// TODO(klinvill): Should try to spawn F* from within this constructor
@@ -198,7 +198,7 @@ export class FStarConnection {
 	}
 
 	// Send a request to F* to check the given code up through a position.
-	partialBufferRequest(code: string, kind: 'verify-to-position' | 'lax-to-position', position: { line: number, column: number }) {
+	partialBufferRequest(code: string, kind: 'verify-to-position' | 'lax-to-position', position: FStarPosition) {
 		this.fullBufferQuery({
 			query: "full-buffer",
 			args: {
@@ -207,7 +207,10 @@ export class FStarConnection {
 				code: code,
 				line: 0,
 				column: 0,
-				"to-position": position
+				"to-position": {
+					line: position[0],
+					column: position[1],
+				},
 			}
 		});
 	}
@@ -306,7 +309,7 @@ export class FStarConnection {
 
 	private handleFBQResponse(msg: any) {
 		const done = msg?.kind === 'message' && msg?.level === 'progress' && msg?.contents?.stage === 'full-buffer-finished';
-		this.onFullBufferResponse(msg);
+		this.onFullBufferResponse(msg, this.fullBufferInProgress!.currentReq);
 		if (done) {
 			const old = this.fullBufferInProgress!;
 			this.fullBufferInProgress = undefined;

server/src/fstar_messages.ts

@@ -93,16 +93,19 @@ export interface IdeCodeFragment {
 	range: FStarRange;
 }
 
-export interface IdeProgress {
-	stage: 'full-buffer-started'
-	| 'full-buffer-fragment-started'
-	| 'full-buffer-fragment-ok'
-	| 'full-buffer-fragment-lax-ok'
-	| 'full-buffer-fragment-failed'
-	| 'full-buffer-finished';
+export interface IdeProgressStartEnd {
+	stage: 'full-buffer-started' | 'full-buffer-finished';
+}
+export interface IdeProgressFragment {
+	stage: 'full-buffer-fragment-started' | 'full-buffer-fragment-failed';
+	ranges: FStarRange;
+}
+export interface IdeProgressFragmentCheck {
+	stage: 'full-buffer-fragment-ok' | 'full-buffer-fragment-lax-ok';
 	ranges: FStarRange;
-	"code-fragment"?: IdeCodeFragment
+	"code-fragment": IdeCodeFragment
 }
+export type IdeProgress = IdeProgressStartEnd | IdeProgressFragment | IdeProgressFragmentCheck;
 
 
 // An auto-complete response

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);