From d437a024e9d52753e13c29a2c20ae756bbc8564c Mon Sep 17 00:00:00 2001 From: Thierry Arnoux <5831830+tirix@users.noreply.github.com> Date: Mon, 30 Oct 2023 10:43:44 +0100 Subject: [PATCH] Header comments, bump `metamath-knife` to v0.3.7 --- Cargo.toml | 2 +- src/main.rs | 3 +- src/statement.rs | 90 ++++++++++++++++++++++++++++++++++++++++++++--- src/sts.rs | 8 +++-- src/sts_parser.rs | 8 +++-- src/toc.hbs | 1 + src/toc.rs | 15 ++++++++ 7 files changed, 114 insertions(+), 13 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index dcdc852..bf20b41 100644 --- 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 index e901418..51f46c2 100644 --- 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 { 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 index 6c2f755..4298321 100644 --- 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!( "
 |- {}
", - &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 { - 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('&', "&") + .replace('<', "<") + .replace('>', ">"), + ); + } + } + CommentItem::LineBreak(_) => { + trim_prev_ws = true; + comment.push_str("

"); + } + // 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!( + "{label}", + label = as_str(&out) + )); + } + CommentItem::Url(_, sp) => { + trim_prev_ws = true; + out.clear(); + parser.unescape_label(sp, &mut out); + comment.push_str(&format!("{url}", url = as_str(&out))); + } + CommentItem::StartHtml(_) => htmls += 1, + CommentItem::EndHtml(_) => htmls -= 1, + CommentItem::StartSubscript(_) => comment.push_str(""), + CommentItem::EndSubscript(_) => comment.push_str(""), + CommentItem::StartItalic(_) => comment.push_str(""), + CommentItem::EndItalic(_) => { + trim_prev_ws = true; + comment.push_str(""); + } + CommentItem::BibTag(sp) => { + trim_prev_ws = false; + comment.push_str(&format!( + "[{tag}]", + file = self.bib_file, + tag = as_str(sp.as_ref(buf)) + )); + } + } + } + comment + } + pub fn render_statement(&self, explorer: String, label: String) -> Option { 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 index e8f889a..869740c 100644 --- 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 index 67c573e..1f70228 100644 --- 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 index f1ba9f4..b9cb62f 100644 --- a/src/toc.hbs +++ b/src/toc.hbs @@ -37,6 +37,7 @@


Table of Contents - {{#each nav.breadcrumb}}{{index}}{{#if index}}.{{/if}}{{/each}} {{name}}

+

{{comment}}

    {{#each children}}
  1. {{name}} diff --git a/src/toc.rs b/src/toc.rs index ae38e76..238dd94 100644 --- 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, explorer: String, link: LinkInfo, children: Vec, @@ -104,16 +107,28 @@ impl Renderer { }) } + fn get_comment(&self, node: &OutlineNodeRef) -> Option { + 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 { 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()