oak_lean/lsp/
mod.rs

1#![doc = include_str!("readme.md")]
2#[cfg(feature = "oak-highlight")]
3pub mod highlighter;
4
5use crate::language::LeanLanguage;
6#[cfg(feature = "lsp")]
7use oak_lsp::{LanguageService, MemoryVfs, WorkspaceManager};
8#[cfg(feature = "lsp")]
9pub struct LeanLanguageService {
10    config: LeanLanguage,
11    vfs: MemoryVfs,
12    workspace: WorkspaceManager,
13}
14#[cfg(feature = "lsp")]
15impl LeanLanguageService {
16    pub fn new(config: LeanLanguage) -> Self {
17        Self { config, vfs: MemoryVfs::default(), workspace: WorkspaceManager::default() }
18    }
19}
20#[cfg(feature = "lsp")]
21impl LanguageService for LeanLanguageService {
22    type Lang = LeanLanguage;
23    type Vfs = MemoryVfs;
24    fn vfs(&self) -> &Self::Vfs {
25        &self.vfs
26    }
27    fn workspace(&self) -> &WorkspaceManager {
28        &self.workspace
29    }
30}
oak_lean/lsp/mod.rs

oak_lean/lsp/
mod.rs
