diff --git a/src/main.rs b/src/main.rs index 5a2ed0d4..d1c4bcba 100644 --- a/src/main.rs +++ b/src/main.rs @@ -27,7 +27,7 @@ use intrinsic::{annotations::init_calculi, distributions::init_distributions, li use procs::add_default_specs; use proof_rules::init_encodings; use resource_limits::{await_with_resource_limits, LimitError, LimitsRef}; -use servers::{CliServer, LspServer, Server, ServerError}; +use servers::{CliServer, LspServer, Server, ServerError, VerifyResult}; use slicing::init_slicing; use thiserror::Error; use timing::DispatchBuilder; @@ -583,8 +583,9 @@ fn verify_files_main( result.print_prove_result(files_mutex, &vc_expr, &mut translate, name); } let status = match &result.prove_result { - ProveResult::Proof => true, - ProveResult::Counterexample(_) | ProveResult::Unknown(_) => false, + ProveResult::Proof => VerifyResult::Verified, + ProveResult::Counterexample(_) => VerifyResult::Failed, + ProveResult::Unknown(_) => VerifyResult::Unknown, }; server .set_verify_status(verify_unit.span, status) @@ -613,16 +614,18 @@ fn verify_files_main( } } - println!(); - let ending = if num_failures == 0 { - " veni, vidi, vici!" - } else { - "" - }; - println!( - "{} verified, {} failed.{}", - num_proven, num_failures, ending - ); + if !options.language_server { + println!(); + let ending = if num_failures == 0 { + " veni, vidi, vici!" + } else { + "" + }; + println!( + "{} verified, {} failed.{}", + num_proven, num_failures, ending + ); + } Ok(num_failures == 0) } diff --git a/src/servers/cli.rs b/src/servers/cli.rs index 5b934244..f48ea779 100644 --- a/src/servers/cli.rs +++ b/src/servers/cli.rs @@ -9,7 +9,7 @@ use crate::{ Options, VerifyError, }; -use super::{unless_fatal_error, Server, ServerError}; +use super::{unless_fatal_error, Server, ServerError, VerifyResult}; pub struct CliServer { werr: bool, @@ -65,7 +65,7 @@ impl Server for CliServer { Ok(()) } - fn set_verify_status(&mut self, _span: Span, _status: bool) -> Result<(), ServerError> { + fn set_verify_status(&mut self, _span: Span, _status: VerifyResult) -> Result<(), ServerError> { // TODO Ok(()) } diff --git a/src/servers/lsp.rs b/src/servers/lsp.rs index db0a0175..63f58f0c 100644 --- a/src/servers/lsp.rs +++ b/src/servers/lsp.rs @@ -17,17 +17,17 @@ use crate::{ VerifyError, }; -use super::{Server, ServerError}; +use super::{Server, ServerError, VerifyResult}; #[derive(Debug, Serialize, Deserialize)] -struct VerifyStatusRequest { +struct VerifyRequest { text_document: VersionedTextDocumentIdentifier, } #[derive(Debug, Serialize, Deserialize)] struct VerifyStatusUpdate { document: VersionedTextDocumentIdentifier, - statuses: Vec<(lsp_types::Range, bool)>, + statuses: Vec<(lsp_types::Range, VerifyResult)>, } /// A connection to an LSP client. @@ -36,7 +36,7 @@ pub struct LspServer { files: Arc>, connection: Connection, diagnostics: Vec, - statuses: HashMap, + statuses: HashMap, } impl LspServer { @@ -84,9 +84,9 @@ impl LspServer { for msg in &receiver { match msg { Message::Request(req) => { - if let "custom/verifyStatus" = req.method.as_str() { + if let "custom/verify" = req.method.as_str() { let (id, params) = req - .extract::("custom/verifyStatus") + .extract::("custom/verify") .map_err(|e| VerifyError::ServerError(e.into()))?; self.project_root = Some(params.text_document.clone()); let files = self.files.lock().unwrap(); @@ -252,7 +252,7 @@ impl Server for LspServer { Ok(()) } - fn set_verify_status(&mut self, span: Span, status: bool) -> Result<(), ServerError> { + fn set_verify_status(&mut self, span: Span, status: VerifyResult) -> Result<(), ServerError> { self.statuses.insert(span, status); self.publish_verify_statuses()?; Ok(()) diff --git a/src/servers/mod.rs b/src/servers/mod.rs index 8d416bb3..6b16e450 100644 --- a/src/servers/mod.rs +++ b/src/servers/mod.rs @@ -16,11 +16,20 @@ mod test; use ariadne::ReportKind; pub use cli::CliServer; pub use lsp::LspServer; +use serde::{Deserialize, Serialize}; #[cfg(test)] pub use test::TestServer; pub type ServerError = Box; +#[derive(Debug, Serialize, Deserialize, Clone, Copy)] +#[serde(rename_all = "lowercase")] +pub enum VerifyResult { + Verified, + Failed, + Unknown, +} + /// A server that serves information to a client, such as the CLI or an LSP /// client. pub trait Server: Send { @@ -36,7 +45,7 @@ pub trait Server: Send { fn add_diagnostic(&mut self, diagnostic: Diagnostic) -> Result<(), VerifyError>; /// Send a verification status message to the client (a custom notification). - fn set_verify_status(&mut self, span: Span, status: bool) -> Result<(), ServerError>; + fn set_verify_status(&mut self, span: Span, status: VerifyResult) -> Result<(), ServerError>; } fn unless_fatal_error(werr: bool, diagnostic: Diagnostic) -> Result { diff --git a/src/servers/test.rs b/src/servers/test.rs index c4afddd7..371aeaa2 100644 --- a/src/servers/test.rs +++ b/src/servers/test.rs @@ -8,13 +8,13 @@ use crate::{ Options, VerifyError, }; -use super::{unless_fatal_error, Server, ServerError}; +use super::{unless_fatal_error, Server, ServerError, VerifyResult}; pub struct TestServer { pub files: Arc>, werr: bool, pub diagnostics: Vec, - pub statuses: HashMap, + pub statuses: HashMap, } impl TestServer { @@ -47,7 +47,7 @@ impl Server for TestServer { Ok(()) } - fn set_verify_status(&mut self, span: Span, status: bool) -> Result<(), ServerError> { + fn set_verify_status(&mut self, span: Span, status: VerifyResult) -> Result<(), ServerError> { self.statuses.insert(span, status); Ok(()) } diff --git a/vscode-ext/src/APIRegister.ts b/vscode-ext/src/APIRegister.ts deleted file mode 100644 index 0fab726e..00000000 --- a/vscode-ext/src/APIRegister.ts +++ /dev/null @@ -1,42 +0,0 @@ -import * as vscode from 'vscode'; - -export const registerFunctions: { [K: string]: Function } = { - "onDidChangeConfiguration": vscode.workspace.onDidChangeConfiguration, - "onDidChangeTextDocument": vscode.workspace.onDidChangeTextDocument, - "onDidSaveTextDocument": vscode.workspace.onDidSaveTextDocument, -} - -export type RegisterType = keyof typeof registerFunctions; - -export default class APIRegister { - - /// Store all registered callbacks in a map to submit them to vscode api later - private static callbackMap = new Map void>>(); - - - /// Register a callback to be called when the vscode api event is triggered - public static register(type: RegisterType, callback: (...args: any[]) => void): void { - this.callbackMap.has(type) ? this.callbackMap.get(type)?.push(callback) : this.callbackMap.set(type, [callback]); - } - - /// Submit all registered callbacks to vscode api - public static submitAll(): void { - - for (const type of this.callbackMap.keys()) { - if (registerFunctions[type] === undefined) { - throw new Error(`The type ${type} is not a valid registration type`); - } - - // All callbacks that we want to register to the specific event from vscode api - const callbackList = this.callbackMap.get(type)!; - - // Collect all the callbacks into one function - const totalCallback = (...args: any[]) => { callbackList.forEach((callback) => callback(...args)) }; - - // Register the function to the vscode api by calling the corresponding event registration function - registerFunctions[type](totalCallback); - } - - } - -} diff --git a/vscode-ext/src/Configuration.ts b/vscode-ext/src/Configuration.ts index 7fa58a21..f44ef188 100644 --- a/vscode-ext/src/Configuration.ts +++ b/vscode-ext/src/Configuration.ts @@ -4,9 +4,9 @@ export const CONFIGURATION_SECTION = 'caesar'; export default class Configuration { - /// Get a configuration value from the configuration file with the given key + /// Get a configuration value from the configuration file with the given key public static get(key: string): any { - const val: any | undefined = vscode.workspace.getConfiguration(CONFIGURATION_SECTION).get(key) + const val = vscode.workspace.getConfiguration(CONFIGURATION_SECTION).get(key) if (val === undefined) { throw new Error(`${key} is not defined in the configuration file`); } @@ -34,13 +34,12 @@ export class ConfigCategory { return Configuration.get(this.getPath() + "." + key); } - } -// Configurations +// Configurations // ------------------------------------------------ -// Root Configurations: +// Root Configurations: export const ViewConfiguration = new ConfigCategory("uI", null); @@ -50,9 +49,3 @@ export const ViewConfiguration = new ConfigCategory("uI", null); export const GutterInformationViewConfig = new ConfigCategory('gutterIcons', ViewConfiguration,); export const StatusBarViewConfig = new ConfigCategory('statusBar', ViewConfiguration); export const InlineGhostTextViewConfig = new ConfigCategory('inlineGhostText', ViewConfiguration); - - - - - - diff --git a/vscode-ext/src/Verifier.ts b/vscode-ext/src/Verifier.ts new file mode 100644 index 00000000..1e2a9849 --- /dev/null +++ b/vscode-ext/src/Verifier.ts @@ -0,0 +1,440 @@ +import { LanguageClientOptions, TextDocumentIdentifier, VersionedTextDocumentIdentifier } from "vscode-languageclient"; +import { LanguageClient, ServerOptions } from "vscode-languageclient/node"; +import { ExtensionContext, Range, StatusBarItem, TextDocument, TextEditorDecorationType } from "vscode"; +import * as vscode from 'vscode'; +import { CONFIGURATION_SECTION, GutterInformationViewConfig, InlineGhostTextViewConfig, StatusBarViewConfig } from "./Configuration"; + +class DocumentMap { + private map: Map = new Map(); + + public insert(document_id: TextDocumentIdentifier, value: T) { + this.map.set(document_id.uri.toString(), [document_id, value]); + } + + public get(document_id: TextDocumentIdentifier): T | undefined { + let res = this.map.get(document_id.uri.toString()); + if (res !== undefined) { + return res[1]; + } + return undefined; + } + + public entries(): Array<[TextDocumentIdentifier, T]> { + return Array.from(this.map.values()); + } +} + +export enum ServerStatus { + Starting, + Ready, + FailedToStart, + Verifying, + Finished, +} + +export enum VerifyResult { + Verified = "verified", + Failed = "failed", + Unknown = "unknown", +} + +export type VerifyStatusNotification = { + document: VersionedTextDocumentIdentifier, + statuses: Array<[vscode.Range, VerifyResult]>, +}; + +export type ComputedPreNotification = { + document: VersionedTextDocumentIdentifier, + pres: Array<[vscode.Range, string]>, +}; + +class CaesarClient { + private client: LanguageClient; + private statusListeners: Array<(status: ServerStatus) => void> = new Array(); + private updateListeners: Array<(document: TextDocumentIdentifier, results: Array<[Range, VerifyResult]>) => void> = new Array(); + private computedPreListeners: Array<(document: TextDocumentIdentifier, results: Array<[Range, string]>) => void> = new Array(); + + constructor(context: ExtensionContext) { + let serverOptions: ServerOptions = { + run: { + command: 'cargo', + args: ['run', '--', '--language-server'], + options: { + }, // TODO!! + }, + debug: { + command: 'cargo', + args: ['run', '--', '--language-server'], + options: { + env: { + ...process.env, + "RUST_LOG": "caesar=info", + "NO_COLOR": "1", + "RUST_BACKTRACE": "1" + } + }, // TODO!! + } + }; + + let clientOptions: LanguageClientOptions = { + diagnosticCollectionName: 'caesar', + documentSelector: [{ scheme: 'file', language: 'heyvl' }], + synchronize: { + // Notify the server about file changes to '.clientrc files contained in the workspace + fileEvents: vscode.workspace.createFileSystemWatcher('**/*.heyvl') + } + }; + + // Create the language client and start the client. + this.client = new LanguageClient( + 'caesar', + 'Caesar', + serverOptions, + clientOptions + ); + context.subscriptions.push(this.client); + + // set up listeners for our custom events + context.subscriptions.push(this.client.onNotification("custom/verifyStatus", (params: VerifyStatusNotification) => { + for (let listener of this.updateListeners) { + listener(params.document, params.statuses); + } + })); + + context.subscriptions.push(this.client.onNotification("custom/computedPre", (params: ComputedPreNotification) => { + for (let listener of this.computedPreListeners) { + listener(params.document, params.pres); + } + })); + + // listen to onDidSaveTextDocument events + context.subscriptions.push(vscode.workspace.onDidSaveTextDocument((document) => { + // TODO: look at setting + this.verify(document); + })); + + // listen to commands + vscode.commands.registerCommand('caesar.restartServer', async () => { + await this.restart(); + }); + + vscode.commands.registerCommand('caesar.startServer', async () => { + await this.start(); + }); + + vscode.commands.registerCommand('caesar.stopServer', async () => { + await this.stop(); + }); + + vscode.commands.registerCommand('caesar.verify', async () => { + let openEditor = vscode.window.activeTextEditor; + if (openEditor) { + this.verify(openEditor.document); + } + }); + } + + async start() { + console.log("Starting Caesar"); + this.notifyStatusUpdate(ServerStatus.Starting); + await this.client.start(); + this.notifyStatusUpdate(ServerStatus.Ready); + } + + async restart() { + console.log("Restarting Caesar"); + this.client.restart(); + } + + async stop() { + console.log("Stopping Caesar"); + this.client.stop(); + } + + async verify(document: TextDocument) { + let documentItem = { + uri: document.uri.toString(), + languageId: document.languageId, + version: document.version, + text: document.getText() + }; + this.notifyStatusUpdate(ServerStatus.Verifying); + await this.client.sendRequest('custom/verify', { text_document: documentItem }); + // TODO: handle errors + this.notifyStatusUpdate(ServerStatus.Finished); + } + + public onStatusUpdate(callback: (status: ServerStatus) => void) { + this.statusListeners.push(callback); + } + + private notifyStatusUpdate(status: ServerStatus) { + for (let listener of this.statusListeners) { + listener(status); + } + } + + public onVerifyResult(callback: (document: TextDocumentIdentifier, results: Array<[Range, VerifyResult]>) => void) { + this.updateListeners.push(callback); + } + + public onComputedPre(callback: (document: TextDocumentIdentifier, results: Array<[Range, string]>) => void) { + this.computedPreListeners.push(callback); + } +} + +export class Verifier { + + public context: ExtensionContext; + public client: CaesarClient; + private statusBar: StatusBarComponent; + private gutterStatus: GutterStatusComponent; + private displayComputedPre: ComputedPreComponent; + + constructor(context: ExtensionContext) { + this.context = context; + this.client = new CaesarClient(context); + this.statusBar = new StatusBarComponent(this); + this.gutterStatus = new GutterStatusComponent(this); + this.displayComputedPre = new ComputedPreComponent(this); + } + + async start() { + await this.client.start(); + } + +} + +class StatusBarComponent { + + private enabled: boolean; + private status: ServerStatus = ServerStatus.Starting; + private view: StatusBarItem; + + constructor(verifier: Verifier) { + // create the view + this.view = vscode.window.createStatusBarItem(vscode.StatusBarAlignment.Left, 99); + verifier.context.subscriptions.push(this.view); + this.view.text = "Caesar"; + + this.view.tooltip = new vscode.MarkdownString( + "[Restart Caesar](command:caesar.restartServer)\n\n" + + "[Start Caesar](command:caesar.startServer)\n\n" + + "[Stop Caesar](command:caesar.stopServer)" + , true); + + // render if enabled + this.enabled = StatusBarViewConfig.get("showStatusBar"); + this.render(); + + // subscribe to config changes + verifier.context.subscriptions.push(vscode.workspace.onDidChangeConfiguration((e: vscode.ConfigurationChangeEvent) => { + if (e.affectsConfiguration(CONFIGURATION_SECTION)) { + this.enabled = StatusBarViewConfig.get("showStatusBar"); + this.render(); + } + })); + + // listen to verifier updates + verifier.client.onStatusUpdate((status) => { + this.status = status; + this.render(); + }); + } + + render() { + if (this.enabled) { + switch (this.status) { + case ServerStatus.Starting: + this.view.text = "$(sync~spin) Starting Caesar..."; + break; + case ServerStatus.Ready: + this.view.text = "$(check) Caesar Ready"; + break; + case ServerStatus.Verifying: + this.view.text = "$(sync~spin) Verifying..."; + break; + case ServerStatus.Finished: + this.view.text = "$(check) Verified"; + break; + } + this.view.show(); + } else { + this.view.hide(); + } + } +} + +class GutterStatusComponent { + + private enabled: boolean; + private status: DocumentMap>; + + private verifyDecType: vscode.TextEditorDecorationType; + private failedDecType: vscode.TextEditorDecorationType; + private unknownDecType: vscode.TextEditorDecorationType; + + constructor(verifier: Verifier) { + // create decorations + this.verifyDecType = vscode.window.createTextEditorDecorationType({ gutterIconSize: "contain", gutterIconPath: verifier.context.asAbsolutePath('images/verified.png') }); + this.failedDecType = vscode.window.createTextEditorDecorationType({ gutterIconSize: "contain", gutterIconPath: verifier.context.asAbsolutePath('images/failed.png') }); + this.unknownDecType = vscode.window.createTextEditorDecorationType({ gutterIconSize: "contain", gutterIconPath: verifier.context.asAbsolutePath('images/unknown.png') }); + + // render if enabled + this.enabled = GutterInformationViewConfig.get("showGutterIcons"); + + this.status = new DocumentMap(); + + // subscribe to config changes + verifier.context.subscriptions.push(vscode.workspace.onDidChangeConfiguration((e: vscode.ConfigurationChangeEvent) => { + if (e.affectsConfiguration(CONFIGURATION_SECTION)) { + this.enabled = StatusBarViewConfig.get("showGutterIcons"); + this.render(); + } + })); + + // render when visible editors change + verifier.context.subscriptions.push(vscode.window.onDidChangeVisibleTextEditors((_visibleEditors) => { + this.render(); + })); + + // listen to status and verify updates + verifier.client.onStatusUpdate((status) => { + if (status == ServerStatus.Verifying) { + for (let [_document, results] of this.status.entries()) { + results.length = 0; + } + this.render(); + } + }); + + verifier.client.onVerifyResult((document, results) => { + this.status.insert(document, results); + this.render(); + }); + } + + render() { + for (let [document_id, results] of this.status.entries()) { + for (let editor of vscode.window.visibleTextEditors) { + if (editor.document.uri.toString() !== document_id.uri) { + continue; + } + + let verifiedProcs: vscode.DecorationOptions[] = []; + let failedProcs: vscode.DecorationOptions[] = []; + let unknownProcs: vscode.DecorationOptions[] = []; + + if (this.enabled) { + for (let [range, result] of results) { + let line = range.start.line; + let gutterRange = new vscode.Range(line, 0, line, 0); + switch (result) { + case VerifyResult.Verified: + verifiedProcs.push({ range: gutterRange, hoverMessage: 'Verified' }); + break; + case VerifyResult.Failed: + failedProcs.push({ range: gutterRange, hoverMessage: 'Not Verified' }); + break; + case VerifyResult.Unknown: + unknownProcs.push({ range: gutterRange, hoverMessage: 'Unknown' }); + break; + } + } + } + + editor.setDecorations(this.verifyDecType, verifiedProcs); + editor.setDecorations(this.failedDecType, failedProcs); + editor.setDecorations(this.unknownDecType, unknownProcs); + } + } + } +} + +class ComputedPreComponent { + + private enabled: boolean; + private computedPres: DocumentMap>; + + private decorationType: TextEditorDecorationType; + + constructor(verifier: Verifier) { + // create decoration + this.decorationType = vscode.window.createTextEditorDecorationType({}); + + // set enabled flag + this.enabled = GutterInformationViewConfig.get("showGutterIcons"); + + this.computedPres = new DocumentMap(); + + // subscribe to config changes + verifier.context.subscriptions.push(vscode.workspace.onDidChangeConfiguration((e: vscode.ConfigurationChangeEvent) => { + if (e.affectsConfiguration(CONFIGURATION_SECTION)) { + this.enabled = InlineGhostTextViewConfig.get("showInlineGhostText"); + this.render(); + } + })); + + // render when visible text editors change + verifier.context.subscriptions.push(vscode.window.onDidChangeVisibleTextEditors((_visibleEditors) => { + this.render(); + })); + + // listen to custom/computedPre notifications + verifier.client.onComputedPre((document, pres) => { + this.computedPres.insert(document, pres); + }); + + // clear all information when a new verification task is started + verifier.client.onStatusUpdate((status) => { + if (status == ServerStatus.Verifying) { + for (let [_document, results] of this.computedPres.entries()) { + results.length = 0; + } + this.render(); + } + }); + + // TODO: listen to content changes to remove lines? + } + + render() { + let backgroundColor = new vscode.ThemeColor('caesar.inlineGhostBackgroundColor'); + let color = new vscode.ThemeColor('caesar.inlineGhostForegroundColor'); + + for (let [document_id, pres] of this.computedPres.entries()) { + for (let editor of vscode.window.visibleTextEditors) { + if (editor.document.uri.toString() !== document_id.uri) { + continue; + } + + let decorations: vscode.DecorationOptions[] = []; + + if (this.enabled) { + for (let [range, text] of pres) { + let line = range.start.line; + if (line === 0) { + continue; + } + let lineAbove = line - 1; + let rangeAbove = new vscode.Range(lineAbove, 0, lineAbove, 0); + if (editor.document.lineAt(lineAbove).text.trim() === '') { + decorations.push({ + range: rangeAbove, + renderOptions: { + after: { + backgroundColor, + color, + contentText: text + } + } + }); + } + } + } + + editor.setDecorations(this.decorationType, decorations); + } + } + } +} diff --git a/vscode-ext/src/extension.ts b/vscode-ext/src/extension.ts index da09751f..f3786c1b 100644 --- a/vscode-ext/src/extension.ts +++ b/vscode-ext/src/extension.ts @@ -1,123 +1,13 @@ // The module 'vscode' contains the VS Code extensibility API // Import the module and reference it with the alias vscode in your code below import * as vscode from 'vscode'; -import * as path from 'path'; -import * as os from 'os'; -import { LanguageClient, LanguageClientOptions, ServerOptions, TransportKind } from 'vscode-languageclient/node'; -import { VerificationManager } from './manager/VerificationManager'; -import { GutterInformationView } from './view/GutterInformationView'; -import { StatusBarView } from './view/StatusBarView'; -import { State, StateManager } from './manager/StateManager'; -import { InlineGhostTextView } from './view/InlineGhostTextView'; -import { ViewCollection } from './view/ViewCollection'; -import APIRegister from './APIRegister'; +import { Verifier } from './Verifier'; - -let client: LanguageClient; // This method is called when your extension is activated // Your extension is activated the very first time the command is executed export function activate(context: vscode.ExtensionContext) { - - let serverExecutable = "cargo" - - // If the extension is launched in debug mode then the debug server options are used - // Otherwise the run options are used - let serverOptions: ServerOptions = { - run: { - command: serverExecutable, - args: ['run', '--', '--language-server'], - options: { cwd: path.resolve(os.homedir(), 'caesar') }, - }, - debug: { - command: serverExecutable, - args: ['run', '--', '--language-server'], - options: { cwd: path.resolve(os.homedir(), 'caesar') }, - } - }; - - // Options to control the language client - let clientOptions: LanguageClientOptions = { - diagnosticCollectionName: 'caesar', - // Register the server for heyvl documents - documentSelector: [{ scheme: 'file', language: 'heyvl' }], - synchronize: { - // Notify the server about file changes to '.clientrc files contained in the workspace - fileEvents: vscode.workspace.createFileSystemWatcher('**/*.heyvl') - } - }; - - // Create the language client and start the client. - client = new LanguageClient( - 'caesar', - 'Caesar', - serverOptions, - clientOptions - ); - - - // Initialize Managers - let verificationManager = new VerificationManager(client); - let stateManager = new StateManager(client); - - // // Initialize UI Views - let viewCollection = new ViewCollection(verificationManager, stateManager, context, client); - - APIRegister.register('onDidSaveTextDocument', (textDocument) => { - if (textDocument.languageId === "heyvl") { - if (stateManager.getState() === State.Starting) { - return - } - const openEditor = vscode.window.visibleTextEditors.filter( - editor => editor.document.uri === textDocument.uri - )[0] - stateManager.setState(State.Verifying); - console.log("Verification Started") - - verificationManager.verify(openEditor, textDocument).then((_) => { - stateManager.setState(State.Finished) - }) - } - }); - - - vscode.commands.registerCommand('caesar.restartServer', async () => { - console.log("Restarting Caesar...") - client.restart() - }); - - vscode.commands.registerCommand('caesar.startServer', async () => { - console.log("Starting Caesar...") - client.start() - }); - - vscode.commands.registerCommand('caesar.stopServer', async () => { - console.log("Stopping Caesar...") - client.stop() - }); - - vscode.commands.registerCommand('caesar.verify', async () => { - const openEditor = vscode.window.activeTextEditor - if (openEditor) { - stateManager.setState(State.Verifying); - console.log("Verification Started") - verificationManager.verify(openEditor, openEditor.document).then((_) => { - stateManager.setState(State.Finished) - }) - } - }); - - - // Submit all received callbacks to vscode api - APIRegister.submitAll(); - // Start the client. This will also launch the server - client.start(); - - console.log('Caesar is now active!'); - - // Add to a list of disposables which are disposed when this extension is deactivated. - context.subscriptions.push(viewCollection); - context.subscriptions.push(client); - + let verifier = new Verifier(context); + verifier.start(); } // This method is called when the extension is deactivated diff --git a/vscode-ext/src/manager/Manager.ts b/vscode-ext/src/manager/Manager.ts deleted file mode 100644 index 2f81de81..00000000 --- a/vscode-ext/src/manager/Manager.ts +++ /dev/null @@ -1,72 +0,0 @@ -// Parent class for Observer-pattern Subjects which we call Managers -export class Manager { - // Observer-pattern subject - - private observers: Observer[] = [] - - - /// Notify the observers with the latest verification status - public notify(update: any) { - this.observers.forEach(observer => observer.receiveUpdate(update)); - } - - /// Subscribe an observer to the VerificationManager - public subscribe(o: Observer) { - if (this.observers.includes(o)) { - return; - } - this.observers.push(o); - } - - /// Subscribe multiple observers to the VerificationManager - public subscribeMany(o: Array) { - o.forEach(observer => this.subscribe(observer)); - } - - /// Unsubscribe an observer from the VerificationManager - public unsubscribe(o: Observer) { - const index = this.observers.indexOf(o); - if (index === -1) { - return; - } - this.observers.splice(index, 1); - } -} - - -export class Observer { - - private callback: (update: any) => void; - private manager: Manager; - private enabled: boolean = true; - - public constructor(manager: Manager, callback: (update: any) => void) { - this.callback = callback; - this.manager = manager; - - this.manager.subscribe(this); - } - - - public receiveUpdate(update: any): void { - this.callback(update); - } - - public disable() { - if (!this.enabled) { - return; - } - this.manager.unsubscribe(this); - } - - public enable() { - if (this.enabled) { - return; - } - this.manager.subscribe(this); - } -} - - - - diff --git a/vscode-ext/src/manager/StateManager.ts b/vscode-ext/src/manager/StateManager.ts deleted file mode 100644 index 2eacdfe5..00000000 --- a/vscode-ext/src/manager/StateManager.ts +++ /dev/null @@ -1,47 +0,0 @@ - -import * as vscode from "vscode"; -import { LanguageClient } from "vscode-languageclient/node"; -import { Manager, Observer } from "./Manager"; - - -export enum State { - Starting, - Ready, - FailedToStart, - Verifying, - Finished, -} - - -// Subject -export class StateManager extends Manager { - - private client: LanguageClient; - - private state: State; - - constructor(client: LanguageClient) { - super(); - this.client = client; - this.state = State.Starting; - this.notify(this.state); - - client.onNotification("custom/serverReady", () => { - this.setState(State.Ready); - }) - } - - - public setState(state: State) { - this.state = state; - this.notify(state); - } - - public getState(): State { - return this.state; - } - -} - - - diff --git a/vscode-ext/src/manager/VerificationManager.ts b/vscode-ext/src/manager/VerificationManager.ts deleted file mode 100644 index 2c10bf53..00000000 --- a/vscode-ext/src/manager/VerificationManager.ts +++ /dev/null @@ -1,34 +0,0 @@ - -import * as vscode from "vscode"; -import { LanguageClient, VersionedTextDocumentIdentifier } from "vscode-languageclient/node"; -import { Manager, Observer } from "./Manager"; -import APIRegister from "../APIRegister"; - - -export type VerificationStatus = { - document: VersionedTextDocumentIdentifier, - statuses: Array<[vscode.Range, boolean]>, -}; - -export class VerificationManager extends Manager { - - private client: LanguageClient; - - - constructor(client: LanguageClient) { - super(); - this.client = client; - } - - public async verify(editor: vscode.TextEditor, document: vscode.TextDocument): Promise { - let documentItem = { - uri: document.uri.toString(), - languageId: document.languageId, - version: document.version, - text: document.getText() - } - await this.client.sendRequest('custom/verifyStatus', { text_document: documentItem }); - } - -} - diff --git a/vscode-ext/src/view/GutterInformationView.ts b/vscode-ext/src/view/GutterInformationView.ts deleted file mode 100644 index 1ada0f8e..00000000 --- a/vscode-ext/src/view/GutterInformationView.ts +++ /dev/null @@ -1,141 +0,0 @@ - -import * as vscode from "vscode"; -import { VerificationManager, VerificationStatus } from "../manager/VerificationManager"; -import { Manager, Observer } from "../manager/Manager"; -import Configuration, { CONFIGURATION_SECTION, ConfigCategory, GutterInformationViewConfig } from "../Configuration"; -import APIRegister from "../APIRegister"; -import { EditorView } from "./View"; -import { VersionedTextDocumentIdentifier } from "vscode-languageclient"; -import { LanguageClient } from "vscode-languageclient/node"; - - - -export enum VerifyStatus { - Verified, - Failed, - Unknown -} - -export enum VerificationColors { - Verified = '#66f542', - Failed = '#f23a3a', - Unknown = '#f7aa57' -} - - -/// The view that displays the verification status of individual (co)procedures in the gutter of the editor with corresponding icons -export class GutterInformationView extends EditorView { - private enabled: boolean; - private verificationObserver: Observer; - - private verifyDecType: vscode.TextEditorDecorationType; - private failedDecType: vscode.TextEditorDecorationType; - private unknownDecType: vscode.TextEditorDecorationType; - - private procStatus?: VerificationStatus; - - constructor(verificationManager: VerificationManager, context: vscode.ExtensionContext, client: LanguageClient) { - super(); - - this.enabled = GutterInformationViewConfig.get("showGutterIcons"); - - this.verifyDecType = vscode.window.createTextEditorDecorationType({ gutterIconSize: "contain", gutterIconPath: context.asAbsolutePath('images/verified.png') }); - this.failedDecType = vscode.window.createTextEditorDecorationType({ gutterIconSize: "contain", gutterIconPath: context.asAbsolutePath('images/failed.png') }); - this.unknownDecType = vscode.window.createTextEditorDecorationType({ gutterIconSize: "contain", gutterIconPath: context.asAbsolutePath('images/unknown.png') }); - - this.verificationObserver = new Observer(verificationManager, (update: VerificationStatus) => { this.receiveVerificationUpdate(update) }); - - // Register the configuration change listener - APIRegister.register("onDidChangeConfiguration", (e: vscode.ConfigurationChangeEvent) => { - if (e.affectsConfiguration(CONFIGURATION_SECTION)) { - console.log("Gutter Config Changed") - if (GutterInformationViewConfig.get("showGutterIcons")) { - this.enable(); - } else { - this.disable(); - } - } - }); - - client.onNotification("custom/verifyStatus", (params: VerificationStatus) => { - this.receiveVerificationUpdate(params); - }) - } - - /// Enable the GutterInformationView - public enable() { - if (this.enabled) { - return; - } - this.enabled = true; - this.verificationObserver.enable(); - this.updateView(vscode.window.activeTextEditor!) - } - - /// Disable the GutterInformationView - public disable() { - if (!this.enabled) { - return; - } - this.enabled = false; - this.verificationObserver.disable(); - this.clearVisibleEditors() - } - - /// Callback function for when the VerificationManager updates - private receiveVerificationUpdate(newStatus: VerificationStatus) { - // Update the decorations - const editor = vscode.window.activeTextEditor; - if (editor) { - this.procStatus = newStatus; - this.updateView(editor); - } - } - - - /// Clear the checkmarks from the given editor - public clearView(editor: vscode.TextEditor) { - editor.setDecorations(this.verifyDecType, []); - editor.setDecorations(this.failedDecType, []); - editor.setDecorations(this.unknownDecType, []); - } - - /// Update the checkmarks based on the latest verification status received from the VerificationManager - public updateView(editor: vscode.TextEditor) { - const verifiedProcs: vscode.DecorationOptions[] = []; - const failedProcs: vscode.DecorationOptions[] = []; - const unknownProcs: vscode.DecorationOptions[] = []; - if (this.enabled && this.procStatus != null && this.procStatus.document.uri == editor.document.uri.toString()) { - for (const proc of this.procStatus.statuses) { - const verified = proc[1]; - - const line = proc[0].start.line; - const range = new vscode.Range(line, 0, line, 0); - if (verified) { - // Put the checkmark before the proc. - verifiedProcs.push({ range, hoverMessage: 'Verified' }); - } else { - // Put the X before the proc. - failedProcs.push({ range, hoverMessage: 'Not Verified' }); - } - } - } - editor.setDecorations(this.verifyDecType, verifiedProcs); - editor.setDecorations(this.failedDecType, failedProcs); - editor.setDecorations(this.unknownDecType, unknownProcs); - } - - - /// Dispose of the GutterInformationView - public dispose() { - this.clearVisibleEditors(); - this.verificationObserver.disable(); - this.verifyDecType.dispose(); - this.failedDecType.dispose(); - this.unknownDecType.dispose(); - } - -} - - - diff --git a/vscode-ext/src/view/InlineGhostTextView.ts b/vscode-ext/src/view/InlineGhostTextView.ts deleted file mode 100644 index 6f6b7fd4..00000000 --- a/vscode-ext/src/view/InlineGhostTextView.ts +++ /dev/null @@ -1,99 +0,0 @@ -import * as vscode from "vscode"; -import { Observer } from "../manager/Manager"; -import { VerificationManager, VerificationStatus } from "../manager/VerificationManager"; -import APIRegister from "../APIRegister"; -import { CONFIGURATION_SECTION, InlineGhostTextViewConfig } from "../Configuration"; -import { EditorView } from "./View"; - - -/// The view that shows the wp/wrt/ert of the respective lines as ghost text in the editor -export class InlineGhostTextView extends EditorView { - - private verificationObserver: Observer; - - - private lineTextMap: Map = new Map([[1, "test"], [2, "test2"], [3, "test3"]]); - - private decorationType: vscode.TextEditorDecorationType; - - constructor(verificationManager: VerificationManager) { - super(); - this.verificationObserver = new Observer(verificationManager, (update: VerificationStatus) => { this.receiveVerificationUpdate(update) }); - this.decorationType = vscode.window.createTextEditorDecorationType({}); - - - APIRegister.register("onDidChangeConfiguration", (e: vscode.ConfigurationChangeEvent) => { - if (e.affectsConfiguration(CONFIGURATION_SECTION)) { - if (InlineGhostTextViewConfig.get("showInlineGhostText")) { - this.enable(); - } else { - this.disable(); - } - } - }); - - } - - public enable() { - this.verificationObserver.enable(); - this.updateView(vscode.window.activeTextEditor!); - } - - public disable() { - this.verificationObserver.disable(); - this.clearVisibleEditors(); - } - - private receiveVerificationUpdate(newStatus: VerificationStatus) { - // Update the decorations - const editor = vscode.window.activeTextEditor; - if (editor) { - this.updateView(editor); - } - } - - public updateText(line: number, text: string) { - this.lineTextMap.set(line, text); - } - - public clearView(editor: vscode.TextEditor) { - editor.setDecorations(this.decorationType, []); - } - - public updateView(editor: vscode.TextEditor) { - const decorations: vscode.DecorationOptions[] = []; - - this.lineTextMap.forEach((text, line) => { - if (this.checkEmptyLine(Math.max(0, line - 1))) { - const range = new vscode.Range(Math.max(0, line - 1), 0, Math.max(0, line - 1), 0); - decorations.push({ - range, renderOptions: { - after: { - backgroundColor: new vscode.ThemeColor('caesar.inlineGhostBackgroundColor'), - color: new vscode.ThemeColor('caesar.inlineGhostForegroundColor'), - contentText: text - } - } - }); - } - }); - - editor.setDecorations(this.decorationType, decorations); - } - - public checkEmptyLine(line: number): boolean { - // Checks if the line above the given line number is empty - const textEditor = vscode.window.activeTextEditor; - if (textEditor && textEditor.document.lineCount > line) { - const lineText = textEditor.document.lineAt(line).text; - return lineText.trim() === ''; - } - return false; - } - - public dispose() { - this.clearVisibleEditors(); - this.decorationType.dispose(); - } - -} diff --git a/vscode-ext/src/view/StatusBarView.ts b/vscode-ext/src/view/StatusBarView.ts deleted file mode 100644 index 3b8d83fb..00000000 --- a/vscode-ext/src/view/StatusBarView.ts +++ /dev/null @@ -1,111 +0,0 @@ -import * as vscode from "vscode"; -import { VerificationStatus } from "../manager/VerificationManager"; -import { Manager, Observer } from "../manager/Manager"; -import { State, StateManager } from "../manager/StateManager"; -import APIRegister from "../APIRegister"; -import { CONFIGURATION_SECTION, StatusBarViewConfig } from "../Configuration"; - - - - - - -/// The view for the status bar at the bottom of the editor -export class StatusBarView { - - private stateObserver: Observer; - - private statusBarItems: Array; - private progressText: vscode.StatusBarItem; - - constructor(stateManager: StateManager) { - - this.stateObserver = new Observer(stateManager, (update: State) => { this.receiveStateUpdate(update) }); - - this.statusBarItems = []; - - this.progressText = vscode.window.createStatusBarItem(vscode.StatusBarAlignment.Left, 99); - this.progressText.text = "caesar"; - - - this.progressText.tooltip = new vscode.MarkdownString( - "[Restart Caesar](command:caesar.restartServer)\n\n" + - "[Start Caesar](command:caesar.startServer)\n\n" + - "[Stop Caesar](command:caesar.stopServer)" - , true); - - this.statusBarItems.push(this.progressText); - - this.showStatusBar(); - - APIRegister.register("onDidChangeConfiguration", (e: vscode.ConfigurationChangeEvent) => { - if (e.affectsConfiguration(CONFIGURATION_SECTION)) { - if (StatusBarViewConfig.get("showStatusBar")) { - this.enable(); - } else { - this.disable(); - } - } - }); - - } - - private showStatusBar() { - for (const statusBarItem of this.statusBarItems) { - statusBarItem.show(); - } - } - - private hideStatusBar() { - for (const statusBarItem of this.statusBarItems) { - statusBarItem.hide(); - } - } - - /// Disable the status bar by hiding it and disabling the observer - public disable() { - this.hideStatusBar(); - this.stateObserver.disable(); - } - - /// Enable the status bar by showing it and enabling the observer - public enable() { - this.showStatusBar(); - this.stateObserver.enable(); - } - - /// Dispose of the status bar - public dispose() { - for (const statusBarItem of this.statusBarItems) { - statusBarItem.dispose(); - } - this.stateObserver.disable(); - } - - /// Update the status bar text based on the latest state received from the StateManager - private receiveStateUpdate(p: State) { - switch (p) { - case State.Starting: - this.progressText.text = StatusBarText.Starting; - break; - case State.Ready: - this.progressText.text = StatusBarText.Ready; - break; - case State.Verifying: - this.progressText.text = StatusBarText.Verifying; - break; - case State.Finished: - this.progressText.text = StatusBarText.Verified; - break; - } - } - -} - - -export enum StatusBarText { - Starting = "$(sync~spin) Starting Caesar...", - Ready = "$(check) Caesar Ready", - Verifying = "$(sync~spin) Verifying...", - Verified = "$(check) Verified" -} diff --git a/vscode-ext/src/view/View.ts b/vscode-ext/src/view/View.ts deleted file mode 100644 index fd72df81..00000000 --- a/vscode-ext/src/view/View.ts +++ /dev/null @@ -1,16 +0,0 @@ -import * as vscode from 'vscode'; - -export abstract class EditorView { - - public abstract updateView(update: any): void; - - public abstract clearView(editor: vscode.TextEditor): void; - - public abstract dispose(): void; - - public clearVisibleEditors() { - const editors = vscode.window.visibleTextEditors; - editors.forEach(editor => this.clearView(editor)); - } - -} diff --git a/vscode-ext/src/view/ViewCollection.ts b/vscode-ext/src/view/ViewCollection.ts deleted file mode 100644 index 1902d044..00000000 --- a/vscode-ext/src/view/ViewCollection.ts +++ /dev/null @@ -1,31 +0,0 @@ -import * as vscode from "vscode"; - -import { StateManager } from "../manager/StateManager"; -import { VerificationManager } from "../manager/VerificationManager"; -import { GutterInformationView } from "./GutterInformationView"; -import { InlineGhostTextView } from "./InlineGhostTextView"; -import { StatusBarView } from "./StatusBarView"; -import { LanguageClient } from "vscode-languageclient/node"; - - -/// A container for all the views in the extension -/// Manages the creation and the on/off configurations of the views -export class ViewCollection { - public gutterInfo: GutterInformationView | null; - public statusBar: StatusBarView | null; - public inlineGhostText: InlineGhostTextView | null; - - - constructor(verificationManager: VerificationManager, stateManager: StateManager, context: vscode.ExtensionContext, client: LanguageClient) { - this.gutterInfo = new GutterInformationView(verificationManager, context, client); - this.statusBar = new StatusBarView(stateManager); - this.inlineGhostText = new InlineGhostTextView(verificationManager); - } - - public dispose() { - this.gutterInfo?.dispose(); - this.statusBar?.dispose(); - this.inlineGhostText?.dispose(); - } - -} diff --git a/vscode-ext/tsconfig.json b/vscode-ext/tsconfig.json index 6954702e..f9592261 100644 --- a/vscode-ext/tsconfig.json +++ b/vscode-ext/tsconfig.json @@ -8,10 +8,11 @@ ], "sourceMap": true, "rootDir": "src", - "strict": true /* enable all strict type-checking options */ + "strict": true, /* enable all strict type-checking options */ /* Additional Checks */ - // "noImplicitReturns": true, /* Report error when not all code paths in function return a value. */ - // "noFallthroughCasesInSwitch": true, /* Report errors for fallthrough cases in switch statement. */ - // "noUnusedParameters": true, /* Report errors on unused parameters. */ + "noImplicitReturns": true, /* Report error when not all code paths in function return a value. */ + "noFallthroughCasesInSwitch": true, /* Report errors for fallthrough cases in switch statement. */ + "noUnusedParameters": true, /* Report errors on unused parameters. */ + } }