vscode-ext: refactor the client

basic user interactions now working with the new server code. client has
been restructured for a simpler and more direct interactions, with
necessary reset handling.

inline ghost text is not functional yet, and the code also needs to be
split into multiple files.

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

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(())
     }

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<Mutex<Files>>,
     connection: Connection,
     diagnostics: Vec<Diagnostic>,
-    statuses: HashMap<Span, bool>,
+    statuses: HashMap<Span, VerifyResult>,
 }
 
 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::<VerifyStatusRequest>("custom/verifyStatus")
+                            .extract::<VerifyRequest>("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(())

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<dyn Error + Send + Sync>;
 
+#[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<Diagnostic, VerifyError> {

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<Mutex<Files>>,
     werr: bool,
     pub diagnostics: Vec<Diagnostic>,
-    pub statuses: HashMap<Span, bool>,
+    pub statuses: HashMap<Span, VerifyResult>,
 }
 
 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(())
     }

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