Header comments, bump metamath-knife to v0.3.7

tirix · Oct 30, 2023 · d437a02 · d437a02
1 parent 483d65d
commit d437a02
Show file tree

Hide file tree

Showing 7 changed files with 114 additions and 13 deletions.
diff --git a/Cargo.toml b/Cargo.toml
@@ -9,7 +9,7 @@ repository = "https://github.com/tirix/metamath-web"
 edition = "2018"
 
 [dependencies]
-metamath-knife = { git = "https://github.com/metamath/metamath-knife", tag = "v0.3.6" }
+metamath-knife = { git = "https://github.com/metamath/metamath-knife", tag = "v0.3.7" }
 handlebars = "4.1.5"
 warp = "0.3.6"
 log = "0.4.14"

diff --git a/src/main.rs b/src/main.rs
@@ -12,7 +12,6 @@ use clap::App as ClapApp;
 use clap::Arg;
 use clap::ArgMatches;
 use metamath_knife::database::DbOptions;
-use metamath_knife::diag::DiagnosticClass;
 use metamath_knife::Database;
 use std::collections::HashMap;
 use std::convert::Infallible;
@@ -97,7 +96,7 @@ fn build_db(args: &ArgMatches) -> Result<Database, String> {
     println!("Starting up...");
     db.parse(start, data);
     db.scope_pass();
-    let diag = db.diag_notations(&[DiagnosticClass::Parse]);
+    let diag = db.diag_notations();
     if !diag.is_empty() {
         return Err(format!("{:?}", diag));
     }

diff --git a/src/statement.rs b/src/statement.rs
@@ -3,12 +3,15 @@ use crate::sts::StsDefinition;
 use crate::toc::NavInfo;
 use crate::uni::UnicodeRenderer;
 use handlebars::Handlebars;
+use metamath_knife::comment_parser::CommentItem;
+use metamath_knife::comment_parser::CommentParser;
 use metamath_knife::proof::ProofTreeArray;
 use metamath_knife::statement::as_str;
 use metamath_knife::statement::StatementRef;
 use metamath_knife::statement::StatementType;
 use metamath_knife::Database;
 use metamath_knife::Formula;
+use metamath_knife::Span;
 use regex::{Captures, Regex};
 use serde::Serialize;
 use std::sync::Arc;
@@ -120,7 +123,7 @@ impl ExpressionRenderer {
         match self {
             ExpressionRenderer::Ascii => Ok(format!(
                 "<pre> |- {}</pre>",
-                &String::from_utf8_lossy(&proof_tree.exprs[tree_index])
+                &String::from_utf8_lossy(&proof_tree.exprs().unwrap()[tree_index])
             )),
             ExpressionRenderer::Unicode(uni) => {
                 uni.render_formula(&ExpressionRenderer::as_formula(
@@ -158,7 +161,7 @@ impl ExpressionRenderer {
         tree_index: usize,
         use_provables: bool,
     ) -> Result<Formula, String> {
-        let formula_string = String::from_utf8_lossy(&proof_tree.exprs[tree_index]);
+        let formula_string = String::from_utf8_lossy(&proof_tree.exprs().unwrap()[tree_index]);
         let nset = database.name_result();
         let grammar = database.grammar_result();
         let typecodes = if use_provables {
@@ -309,6 +312,85 @@ impl Renderer {
         comment.to_string()
     }
 
+    pub(crate) fn render_comment_new(&self, buf: &[u8], span: Span) -> String {
+        let mut parser = CommentParser::new(buf, span);
+        let mut htmls = 0;
+        let mut trim_prev_ws = true;
+        let mut comment = "".to_string();
+        while let Some(item) = parser.next() {
+            let mut out = vec![];
+            match item {
+                CommentItem::Text(sp) => {
+                    out.clear();
+                    parser.unescape_text(sp, &mut out);
+                    let mut s = std::str::from_utf8(&out).unwrap();
+                    if trim_prev_ws {
+                        const CLOSING_PUNCTUATION: &str = ".,;)?!:]'\"_-";
+                        s = s.trim_start();
+                        trim_prev_ws = false;
+                        if matches!(s.chars().next(), Some(c) if !CLOSING_PUNCTUATION.contains(c)) {
+                            comment.push(' ');
+                        }
+                    }
+                    if htmls == 0 {
+                        comment.push_str(s);
+                    } else {
+                        comment.push_str(
+                            &s.replace('&', "&amp;")
+                                .replace('<', "&lt;")
+                                .replace('>', "&gt;"),
+                        );
+                    }
+                }
+                CommentItem::LineBreak(_) => {
+                    trim_prev_ws = true;
+                    comment.push_str("<p style=\"margin-bottom:0em\">");
+                }
+                // TODO : math mode: gather symbols, defer to expression renderer
+                CommentItem::StartMathMode(_) => {}
+                CommentItem::EndMathMode(_) => {}
+                CommentItem::MathToken(sp) => {
+                    out.clear();
+                    parser.unescape_math(sp, &mut out);
+                    // TODO! comment.push_str(self.html_defs[&*out]);
+                }
+                CommentItem::Label(_, sp) => {
+                    trim_prev_ws = true;
+                    out.clear();
+                    parser.unescape_label(sp, &mut out);
+                    comment.push_str(&format!(
+                        "<a href=\"{label}.html\" class=\"label\">{label}</a>",
+                        label = as_str(&out)
+                    ));
+                }
+                CommentItem::Url(_, sp) => {
+                    trim_prev_ws = true;
+                    out.clear();
+                    parser.unescape_label(sp, &mut out);
+                    comment.push_str(&format!("<a href=\"{url}\">{url}</a>", url = as_str(&out)));
+                }
+                CommentItem::StartHtml(_) => htmls += 1,
+                CommentItem::EndHtml(_) => htmls -= 1,
+                CommentItem::StartSubscript(_) => comment.push_str("<sub><font size=\"-1\">"),
+                CommentItem::EndSubscript(_) => comment.push_str("</font></sub>"),
+                CommentItem::StartItalic(_) => comment.push_str("<em>"),
+                CommentItem::EndItalic(_) => {
+                    trim_prev_ws = true;
+                    comment.push_str("</em>");
+                }
+                CommentItem::BibTag(sp) => {
+                    trim_prev_ws = false;
+                    comment.push_str(&format!(
+                        "[<a href=\"{file}#{tag}\">{tag}</a>]",
+                        file = self.bib_file,
+                        tag = as_str(sp.as_ref(buf))
+                    ));
+                }
+            }
+        }
+        comment
+    }
+
     pub fn render_statement(&self, explorer: String, label: String) -> Option<String> {
         let sref = self.db.statement(label.as_bytes())?;
         let expression_renderer = self.get_expression_renderer(explorer.clone())?;
@@ -350,7 +432,7 @@ impl Renderer {
                                 .unwrap_or_else(|e| {
                                     format!(
                                         "Could not format {} : {}",
-                                        &String::from_utf8_lossy(&proof_tree.exprs[cur]),
+                                        &String::from_utf8_lossy(&proof_tree.exprs().unwrap()[cur]),
                                         e
                                     )
                                 }),
@@ -374,7 +456,7 @@ impl Renderer {
                                 .unwrap_or_else(|e| {
                                     format!(
                                         "Could not format {} : {}",
-                                        &String::from_utf8_lossy(&proof_tree.exprs[cur]),
+                                        &String::from_utf8_lossy(&proof_tree.exprs().unwrap()[cur]),
                                         e
                                     )
                                 }),

diff --git a/src/sts.rs b/src/sts.rs
@@ -160,9 +160,11 @@ impl StsDefinition {
                         .database
                         .grammar_result()
                         .parse_formula(
-                            &mut tokens.map(|t| FormulaToken {
-                                symbol: nset.get_atom(&t),
-                                span: metamath_knife::Span::NULL,
+                            &mut tokens.map(|t| {
+                                Ok(FormulaToken {
+                                    symbol: nset.get_atom(&t),
+                                    span: metamath_knife::Span::NULL,
+                                })
                             }),
                             &[typecode],
                             false,

diff --git a/src/sts_parser.rs b/src/sts_parser.rs
@@ -38,9 +38,11 @@ impl StsScheme {
         };
         let formula = grammar
             .parse_formula(
-                &mut symbols.into_iter().skip(1).map(|t| FormulaToken {
-                    symbol: t,
-                    span: Span::NULL,
+                &mut symbols.into_iter().skip(1).map(|t| {
+                    Ok(FormulaToken {
+                        symbol: t,
+                        span: Span::NULL,
+                    })
                 }),
                 typecodes,
                 true,

diff --git a/src/toc.hbs b/src/toc.hbs
@@ -37,6 +37,7 @@
 		</nav>
 		<hr />
 		<h2>Table of Contents - {{#each nav.breadcrumb}}{{index}}{{#if index}}.{{/if}}{{/each}} {{name}}</h2>
+		<p>{{comment}}</p>
 		<ol class="toc">
 			{{#each children}}
 				<li><a href="{{link}}" {{#if stmt_level}}class="label"{{/if}}>{{name}}</a>

diff --git a/src/toc.rs b/src/toc.rs
@@ -1,3 +1,5 @@
+use std::ops::Bound;
+
 use crate::statement::Renderer;
 use crate::statement::TypesettingInfo;
 use metamath_knife::outline::OutlineNodeRef;
@@ -9,6 +11,7 @@ use serde::Serializer;
 pub(crate) struct TocInfo {
     nav: NavInfo,
     name: String,
+    comment: Option<String>,
     explorer: String,
     link: LinkInfo,
     children: Vec<ChapterInfo>,
@@ -104,16 +107,28 @@ impl Renderer {
         })
     }
 
+    fn get_comment(&self, node: &OutlineNodeRef) -> Option<String> {
+        let current_address = node.get_statement().address();
+        let next_statement = self
+            .db
+            .statements_range_address((Bound::Excluded(current_address), Bound::Unbounded))
+            .next()?;
+        let comment = next_statement.as_heading_comment()?;
+        Some(self.render_comment_new(&next_statement.segment().segment.buffer, comment.content))
+    }
+
     pub fn render_toc(&self, explorer: String, chapter_ref: usize) -> Option<String> {
         let node = if chapter_ref == 0 {
             self.db.root_outline_node()
         } else {
             self.db.get_outline_node_by_ref(chapter_ref)
         };
+        let comment = self.get_comment(&node);
         let info = TocInfo {
             nav: self.get_nav(&node),
             explorer,
             name: node.get_name().to_string(),
+            comment,
             link: (&node).into(),
             children: node
                 .children_iter()