Skip to content

Commit

Permalink
vscode-ext: register correct spans in lsp server
Browse files Browse the repository at this point in the history
before, we registered the wrong proc spans in the lsp server. this
resulted in the extension thinking there were still "todo" procs left.
  • Loading branch information
Philipp15b committed Jan 22, 2025
1 parent e61cbbf commit dacd5e2
Show file tree
Hide file tree
Showing 2 changed files with 6 additions and 4 deletions.
3 changes: 1 addition & 2 deletions src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -674,12 +674,11 @@ fn verify_files_main(
// Register all relevant source units with the server
for source_unit in &mut source_units {
let source_unit = source_unit.enter();

match *source_unit {
SourceUnit::Decl(ref decl) => {
// only register procs since we do not check any other decls
if let DeclKind::ProcDecl(proc_decl) = decl {
server.register_source_unit(proc_decl.borrow().span)?;
server.register_source_unit(proc_decl.borrow().name.span)?;
}
}
SourceUnit::Raw(ref block) => server.register_source_unit(block.span)?,
Expand Down
7 changes: 5 additions & 2 deletions src/servers/lsp.rs
Original file line number Diff line number Diff line change
Expand Up @@ -328,14 +328,17 @@ impl Server for LspServer {
translate: &mut TranslateExprs<'smt, 'ctx>,
) -> Result<(), ServerError> {
result.emit_diagnostics(span, self, translate)?;
self.statuses
let prev = self
.statuses
.insert(span, VerifyResult::from_prove_result(&result.prove_result));
assert!(prev.is_some());
self.publish_verify_statuses()?;
Ok(())
}

fn handle_not_checked(&mut self, span: Span) -> Result<(), ServerError> {
self.statuses.insert(span, VerifyResult::Unknown);
let prev = self.statuses.insert(span, VerifyResult::Unknown);
assert!(prev.is_some());
self.publish_verify_statuses()?;
Ok(())
}
Expand Down

0 comments on commit dacd5e2

Please sign in to comment.