Xi ropes for MMP

metamath-lsp/Cargo.toml

@@ -13,10 +13,10 @@ categories = ["command-line-utilities", "development-tools", "mathematics"]
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-metamath-knife = { git = "https://github.com/david-a-wheeler/metamath-knife", tag = "v0.3.2" }
+# metamath-knife = { git = "https://github.com/david-a-wheeler/metamath-knife", tag = "v0.3.3" }
+metamath-knife = { path = "../../metamath-knife" }
 lsp-server = "0.5"
 lsp-types = "0.92"
-lsp-text = "0.3"
 xi-rope = "0.3"
 crossbeam = "0.8"
 futures = { version = "0.3", features = ["thread-pool"] }
@@ -27,9 +27,13 @@ serde_json = "1.0"
 serde_repr = "0.1"
 pathdiff = "0.2"
 lazy_static = "1.4"
-# simplelog = "0.11"
+simplelog = "0.11"
 log = "0.4"
 
+# Specific to proofs
+regex = { version = "1.5", default-features = false, features = ["std", "perf"] }
+memchr = "2.4"
+
 [[bin]]
 name = "mm-lsp-server"
 path = "src/main.rs"

metamath-lsp/src/definition.rs

@@ -1,11 +1,11 @@
 //! Provides hover information
 
-use crate::rope_ext::RopeExt;
 use crate::server::word_at;
 use crate::util::FileRef;
 use crate::vfs::Vfs;
 use crate::ServerError;
 use lsp_types::*;
+use metamath_knife::grammar::FormulaToken;
 use metamath_knife::Database;
 use metamath_knife::Span;
 use metamath_knife::StatementRef;
@@ -26,7 +26,11 @@ pub(crate) fn find_statement<'a>(token: &'a [u8], db: &'a Database) -> Option<St
                 // TODO - this could be provided as a utility by metamath-knife wihtout having to build a formula
                 let grammar = db.grammar_result();
                 if let Ok(formula) = grammar.parse_formula(
-                    &mut [symbol.atom].into_iter(),
+                    &mut [FormulaToken {
+                        symbol: symbol.atom,
+                        span: Span::default(),
+                    }]
+                    .into_iter(),
                     &grammar.typecodes(),
                     nset,
                 ) {
@@ -53,21 +57,21 @@ pub(crate) fn span_range(
     db: &Database,
 ) -> Option<Range> {
     let path: PathBuf = db.statement_source_name(stmt.address()).into();
-    let source = vfs.source(path.into()).ok()?;
+    let source = vfs.source(path.into(), db).ok()?;
     Some(Range::new(
-        source.text.byte_to_lsp_position(span.start as usize),
-        source.text.byte_to_lsp_position(span.end as usize),
+        source.byte_to_lsp_position(span.start as usize),
+        source.byte_to_lsp_position(span.end as usize),
     ))
 }
 
 pub(crate) fn stmt_location(stmt: StatementRef<'_>, vfs: &Vfs, db: &Database) -> Option<Location> {
     let path: PathBuf = db.statement_source_name(stmt.address()).into();
-    let source = vfs.source(path.clone().into()).ok()?;
+    let source = vfs.source(path.clone().into(), db).ok()?;
     let uri = Url::from_file_path(path.canonicalize().ok()?).ok()?;
     let span = stmt.span();
     let range = Range::new(
-        source.text.byte_to_lsp_position(span.start as usize),
-        source.text.byte_to_lsp_position(span.end as usize),
+        source.byte_to_lsp_position(span.start as usize),
+        source.byte_to_lsp_position(span.end as usize),
     );
     Some(Location { uri, range })
 }
@@ -78,7 +82,7 @@ pub(crate) fn definition(
     vfs: &Vfs,
     db: Database,
 ) -> Result<Option<Location>, ServerError> {
-    let text = vfs.source(path)?;
+    let text = vfs.source(path, &db)?;
     let (word, _) = word_at(pos, text);
     if let Some(stmt) = find_statement(word.as_bytes(), &db) {
         Ok(stmt_location(stmt, vfs, &db))

metamath-lsp/src/hover.rs

@@ -77,7 +77,7 @@ pub(crate) fn hover(
     vfs: &Vfs,
     db: Database,
 ) -> Result<Option<Hover>, ServerError> {
-    let text = vfs.source(path)?;
+    let text = vfs.source(path, &db)?;
     let (word, range) = word_at(pos, text);
     if let Some(stmt) = find_statement(word.as_bytes(), &db) {
         Ok(Some(Hover {

metamath-lsp/src/main.rs

@@ -4,6 +4,7 @@ mod definition;
 mod diag;
 mod hover;
 mod outline;
+mod proof;
 mod references;
 mod rope_ext;
 mod server;
@@ -119,21 +120,21 @@ impl CondvarExt for std::sync::Condvar {
     }
 }
 
-// fn setup_log(debug: bool) {
-//     let level = if  {
-//         LevelFilter::Debug
-//     } else {
-//         LevelFilter::Info
-//     };
-//     use {
-//         simplelog::{Config, WriteLogger},
-//         std::fs::File,
-//     };
-//     std::env::set_var("RUST_BACKTRACE", "1");
-//     if let Ok(f) = File::create("lsp.log") {
-//         let _ = WriteLogger::init(level, Config::default(), f);
-//     }
-// }
+fn setup_log(debug: bool) {
+    let level = if debug {
+        LevelFilter::Debug
+    } else {
+        LevelFilter::Info
+    };
+    use {
+        simplelog::{Config, WriteLogger},
+        std::fs::File,
+    };
+    std::env::set_var("RUST_BACKTRACE", "1");
+    if let Ok(f) = File::create("lsp.log") {
+        let _ = WriteLogger::init(level, Config::default(), f);
+    }
+}
 
 /// Main entry point for the Metamath language server.
 ///
@@ -174,8 +175,12 @@ pub fn main() {
                 .takes_value(true)
                 .validator(positive_integer),
         )
+        .arg(
+            Arg::with_name("worksheet")
+                .help("Loads a worksheet and exits")
+                .required(false),
+        )
         .get_matches();
-    // setup_log(matches.is_present("debug"));
     let db_file_name = matches.value_of("database").unwrap_or("None");
     let job_count = usize::from_str(matches.value_of("jobs").unwrap_or("1"))
         .expect("validator should check this");
@@ -186,7 +191,21 @@ pub fn main() {
         jobs: job_count,
         ..Default::default()
     };
+    if let Some(proof_file_name) = matches.value_of("worksheet") {
+        let mut db = metamath_knife::Database::new(options);
+        db.parse(db_file_name.into(), Vec::new());
+        db.name_pass();
+        db.scope_pass();
+        db.outline_pass();
+        db.stmt_parse_pass();
+        let worksheet_file =
+            std::fs::File::open(proof_file_name).expect("Could not open proof file");
+        let _worksheet = crate::proof::ProofWorksheet::from_reader(worksheet_file, &db);
+        println!("Successfully loaded worksheet.");
+        std::process::exit(1);
+    }
     SERVER.init(options, db_file_name);
+    setup_log(matches.is_present("debug"));
 
     info!("Starting server");
     if let Err(e) = SERVER.start() {

metamath-lsp/src/proof/mod.rs

@@ -0,0 +1,6 @@
+mod proof_rope;
+mod step;
+mod worksheet;
+
+pub use proof_rope::ProofRope;
+pub use worksheet::ProofWorksheet;