oak_lean/parser/
mod.rs

1/// Element types and tree structure definitions for Lean.
2pub mod element_type;
3
4use crate::{language::LeanLanguage, lexer::LeanLexer, parser::element_type::LeanElementType};
5use oak_core::{
6    parser::{ParseCache, ParseOutput, Parser, ParserState, parse_with_lexer},
7    source::{Source, TextEdit},
8};
9
10pub(crate) type State<'a, S> = ParserState<'a, LeanLanguage, S>;
11
12/// Parser implementation for the Lean language.
13pub struct LeanParser<'config> {
14    pub(crate) config: &'config LeanLanguage,
15}
16
17impl<'config> LeanParser<'config> {
18    /// Creates a new instance of the Lean parser with the given configuration.
19    pub fn new(config: &'config LeanLanguage) -> Self {
20        Self { config }
21    }
22}
23
24impl<'config> Parser<LeanLanguage> for LeanParser<'config> {
25    fn parse<'a, S: Source + ?Sized>(&self, text: &'a S, edits: &[TextEdit], cache: &'a mut impl ParseCache<LeanLanguage>) -> ParseOutput<'a, LeanLanguage> {
26        let lexer = LeanLexer::new(&self.config);
27        parse_with_lexer(&lexer, text, edits, cache, |state| {
28            let checkpoint = state.checkpoint();
29
30            while state.not_at_end() {
31                state.advance();
32            }
33
34            Ok(state.finish_at(checkpoint, LeanElementType::Root))
35        })
36    }
37}
oak_lean/parser/mod.rs

oak_lean/parser/
mod.rs
