Rename IdeError to IdeDiagnostic.

FStarLang · Apr 3, 2024 · ecd63b4 · ecd63b4
1 parent 8ecd240
commit ecd63b4
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 8 deletions.
diff --git a/server/src/fstar_handlers.ts b/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 { IdeLookupResponseResponse, IdeProofState, IdeError, IdeProgress, IdeAutoCompleteOptions, FStarRange } from './fstar_messages';
+import { IdeLookupResponseResponse, IdeProofState, IdeDiagnostic, IdeProgress, IdeAutoCompleteOptions, FStarRange } from './fstar_messages';
 import { mkPosition, fstarRangeAsRange, qualifyFilename } from './utils';
 
 
@@ -129,7 +129,7 @@ export function handleIdeProgress(textDocument: TextDocument, contents: IdeProgr
 
 // If we get errors and warnings from F*, we send them to VSCode as diagnostics,
 // which will show them as squiggles in the editor.
-export function handleIdeDiagnostics(textDocument: TextDocument, response: IdeError[], lax: boolean, server: Server) {
+export function handleIdeDiagnostics(textDocument: TextDocument, response: IdeDiagnostic[], lax: boolean, server: Server) {
 	function ideErrorLevelAsDiagnosticSeverity(level: string): DiagnosticSeverity {
 		switch (level) {
 			case "warning": return DiagnosticSeverity.Warning;

diff --git a/server/src/fstar_messages.ts b/server/src/fstar_messages.ts
@@ -81,9 +81,7 @@ export interface IdeProofStateGoal {
 
 // IDEError: fstar.exe sends this message when reporting errors and warnings
 //
-// TODO(klinvill): These status messages aren't necessarily errors. Maybe should
-// be renamed to `IdeDiagnostic` (following the `handleIdeDiagnostics` name)?
-export interface IdeError {
+export interface IdeDiagnostic {
 	message: string;
 	number: number;
 	level: 'warning' | 'error' | 'info';
@@ -155,7 +153,7 @@ export interface IdeLookupResponse extends IdeQueryResponse {
 
 // Documented at https://github.com/FStarLang/FStar/wiki/Editor-support-for-F*#push
 export interface IdeDiagnosticsResponse extends IdeQueryResponse {
-	response: IdeError[];
+	response: IdeDiagnostic[];
 }
 
 // Replies stemming from full-buffer interruptions seem to have an empty (null)

diff --git a/server/src/server.ts b/server/src/server.ts
@@ -34,7 +34,7 @@ import { formatIdeProofState, fstarRangeAsRange, mkPosition, qualifyFilename, ra
 import { ClientConnection } from './client_connection';
 import { FStarConnection, StreamedResult } from './fstar_connection';
 import { FStar } from './fstar';
-import { FStarRange, IdeProofState, IdeProgress, IdeError, FullBufferQueryResponse } from './fstar_messages';
+import { FStarRange, IdeProofState, IdeProgress, IdeDiagnostic, FullBufferQueryResponse } from './fstar_messages';
 import { handleIdeDiagnostics, handleIdeProgress, handleIdeProofState } from './fstar_handlers';
 
 // LSP Server
@@ -319,7 +319,7 @@ export class Server {
 			if (!response.response) {
 				console.info("Query cancelled");
 			} else if (Array.isArray(response.response)) {
-				handleIdeDiagnostics(textDocument, response.response as IdeError[], lax === 'lax', this);
+				handleIdeDiagnostics(textDocument, response.response as IdeDiagnostic[], lax === 'lax', this);
 			} else {
 				// ignore
 			}