Support module responses to lookup queries.

Fixes #36.

server/src/fstar_connection.ts

@@ -10,7 +10,7 @@ import { setTimeout } from 'timers/promises';
 
 import { FStar, FStarConfig } from './fstar';
 import { isProtocolInfo, ProtocolInfo, FullBufferQuery, LookupQuery, VfsAdd, AutocompleteRequest, CancelRequest,
-	FullBufferQueryResponse, IdeSymbolResponse, IdeAutoCompleteResponse, IdeProgressResponse, IdeVfsAddResponse, IdeResponse} from './fstar_messages';
+	FullBufferQueryResponse, IdeLookupResponse, IdeAutoCompleteResponse, IdeProgressResponse, IdeVfsAddResponse, IdeResponse} from './fstar_messages';
 
 // For full-buffer queries, F* chunks the buffer into fragments and responds
 // with several messages, one for each fragment until the first failing
@@ -188,7 +188,7 @@ export class FStarConnection {
 	//
 	// For more details, see:
 	// https://github.com/FStarLang/FStar/wiki/Editor-support-for-F*#lookup
-	async lookupQuery(filePath: string, position: Position, word: string): Promise<IdeSymbolResponse> {
+	async lookupQuery(filePath: string, position: Position, word: string): Promise<IdeLookupResponse> {
 		const query: LookupQuery = {
 			query: "lookup",
 			args: {

server/src/fstar_handlers.ts

@@ -13,7 +13,7 @@ import * as crypto from 'crypto';
 
 import { Server } from './server';
 import { StatusOkMessage, ok_kind } from './client_connection';
-import { IdeSymbol, IdeProofState, IdeError, IdeProgress, IdeAutoCompleteOptions, FStarRange } from './fstar_messages';
+import { IdeLookupResponseResponse, IdeProofState, IdeError, IdeProgress, IdeAutoCompleteOptions, FStarRange } from './fstar_messages';
 import { mkPosition, fstarRangeAsRange, qualifyFilename } from './utils';
 
 

server/src/fstar_messages.ts

@@ -40,6 +40,14 @@ export interface IdeSymbol {
 	"symbol-range"?: FStarRange;
 	symbol: string;
 }
+export interface IdeModule {
+	kind: 'module';
+	name: string;
+	path: string;
+	loaded: boolean;
+}
+export type IdeLookupResponseResponse =
+	IdeSymbol | IdeModule;
 
 // IdeProofState: fstar.exe sends informative messages when running tactics
 // The server does not explicitly request the proof state---these messages
@@ -141,8 +149,8 @@ export interface IdeProofStateResponse extends IdeQueryMessage {
 }
 
 // Documented at https://github.com/FStarLang/FStar/wiki/Editor-support-for-F*#lookup
-export interface IdeSymbolResponse extends IdeQueryResponse {
-	response: IdeSymbol;
+export interface IdeLookupResponse extends IdeQueryResponse {
+	response: IdeLookupResponseResponse;
 }
 
 // Documented at https://github.com/FStarLang/FStar/wiki/Editor-support-for-F*#push
@@ -166,11 +174,11 @@ export interface IdeVfsAddResponse extends IdeQueryResponse {
 	response: null;
 }
 
-export type IdeResponse = IdeProgressResponse | IdeStatusResponse | IdeProofStateResponse | IdeSymbolResponse | IdeDiagnosticsResponse | IdeInterruptedResponse | IdeAutoCompleteResponse;
+export type IdeResponse = IdeProgressResponse | IdeStatusResponse | IdeProofStateResponse | IdeLookupResponse | IdeDiagnosticsResponse | IdeInterruptedResponse | IdeAutoCompleteResponse;
 
 // Most queries seem to have only one kind of expected response, but full-buffer
 // queries can respond with a large variety of messages.
-export type FullBufferQueryResponse = IdeProgressResponse | IdeStatusResponse | IdeProofStateResponse | IdeSymbolResponse | IdeDiagnosticsResponse | IdeInterruptedResponse;
+export type FullBufferQueryResponse = IdeProgressResponse | IdeStatusResponse | IdeProofStateResponse | IdeLookupResponse | IdeDiagnosticsResponse | IdeInterruptedResponse;
 
 ////////////////////////////////////////////////////////////////////////////////////
 // Request messages in the IDE protocol that fstar.exe uses

server/src/server.ts

@@ -526,22 +526,30 @@ export class Server {
 		// The filename '<input>' here must be exactly the same the we used in the full buffer request.
 		const result = await conn.lookupQuery('<input>', textDocumentPosition.position, word.word);
 		if (result.status !== 'success') return;
-		return {
-			contents: {
-				kind: 'markdown',
-				value:
-					"```fstar\n" +
-					result.response.name + ":\n" +
-					result.response.type + "\n" +
-					"```\n"
-			},
-		};
+		switch (result.response.kind) {
+			case 'symbol': return {
+				contents: {
+					kind: 'markdown',
+					value:
+						"```fstar\n" +
+						result.response.name + ":\n" +
+						result.response.type + "\n" +
+						"```\n"
+				},
+			};
+			case 'module': return {
+				contents: {
+					kind: 'markdown',
+					value: "```fstar\nmodule "+result.response.name+"\n```\n"
+				},
+			};
+		}
 	}
 
 	// The onDefinition handler is called when the user clicks on a symbol
 	// It's very similar to the onHover handler, except that it returns a
 	// LocationLink object instead of a Hover object
-	private async onDefinition(defParams: DefinitionParams): Promise<LocationLink[]> {
+	private async onDefinition(defParams: DefinitionParams): Promise<LocationLink[] | undefined> {
 		const textDoc = this.getDocument(defParams.textDocument.uri);
 		if (!textDoc) { return []; }
 		const lax = this.configurationSettings.flyCheck ? 'lax' : undefined;
@@ -551,13 +559,22 @@ export class Server {
 		// The filename '<input>' here must be exactly the same the we used in the full buffer request.
 		const result = await conn.lookupQuery('<input>', defParams.position, word.word);
 		if (result.status !== 'success') return [];
-		const defined_at = result.response["defined-at"];
-		const range = fstarRangeAsRange(defined_at);
-		return [{
-			targetUri: qualifyFilename(defined_at.fname, textDoc.uri, this),
-			targetRange: range,
-			targetSelectionRange: range,
-		}];
+		if (result.response.kind === 'symbol') {
+			const defined_at = result.response["defined-at"];
+			const range = fstarRangeAsRange(defined_at);
+			return [{
+				targetUri: qualifyFilename(defined_at.fname, textDoc.uri, this),
+				targetRange: range,
+				targetSelectionRange: range,
+			}];
+		} else if (result.response.kind === 'module') {
+			const range: Range = {start: {line: 0, character: 0}, end: {line: 0, character: 0}};
+			return [{
+				targetUri: qualifyFilename(result.response.path, textDoc.uri, this),
+				targetRange: range,
+				targetSelectionRange: range,
+			}];
+		}
 	}
 
 	private async onDocumentRangeFormatting(formatParams: DocumentRangeFormattingParams) {

server/src/utils.ts

@@ -11,7 +11,7 @@ import * as fs from 'fs';
 import * as util from 'util';
 
 import { Server } from './server';
-import { FStarPosition, FStarRange, IdeProofState, IdeProofStateContextualGoal, IdeSymbol } from './fstar_messages';
+import { FStarPosition, FStarRange, IdeProofState, IdeProofStateContextualGoal, IdeLookupResponseResponse } from './fstar_messages';
 
 ////////////////////////////////////////////////////////////////////////////////////
 // Range utilities