From 83df7928ab801cfde2af2ed776c88cdc942e4bbc Mon Sep 17 00:00:00 2001 From: Thierry Arnoux <5831830+tirix@users.noreply.github.com> Date: Sat, 11 Nov 2023 23:59:32 +0100 Subject: [PATCH] Fmt --- src/statement.rs | 49 ++++++++++++++++++++++++++++++------------------ src/sts.rs | 3 ++- 2 files changed, 33 insertions(+), 19 deletions(-) diff --git a/src/statement.rs b/src/statement.rs index 4be6471..e4a6d15 100644 --- a/src/statement.rs +++ b/src/statement.rs @@ -87,10 +87,17 @@ impl ExpressionRenderer { use_provables: bool, ) -> Result { match self { - ExpressionRenderer::Ascii => self.render_formula(&self.get_formula(sref, database, use_provables)?, database, use_provables), + ExpressionRenderer::Ascii => self.render_formula( + &self.get_formula(sref, database, use_provables)?, + database, + use_provables, + ), ExpressionRenderer::Unicode(uni) => uni.render_statement(sref), #[cfg(feature = "sts")] - ExpressionRenderer::Sts(sts) => sts.render_formula(&self.get_formula(sref, database, use_provables)?, use_provables) + ExpressionRenderer::Sts(sts) => sts.render_formula( + &self.get_formula(sref, database, use_provables)?, + use_provables, + ), } } @@ -103,26 +110,28 @@ impl ExpressionRenderer { ) -> Result { if use_provables { database - .stmt_parse_result() - .get_formula(sref) - .ok_or("Unknown statement".into()).cloned() + .stmt_parse_result() + .get_formula(sref) + .ok_or("Unknown statement".into()) + .cloned() } else { let nset = database.name_result(); let grammar = database.grammar_result(); let mut tokens = sref.math_iter(); let _typecode = nset.get_atom(&tokens.next().unwrap()); - grammar.parse_formula( - &mut tokens.map(|t| { - Ok(FormulaToken { - symbol: nset.get_atom(&t), - span: metamath_knife::Span::NULL, - }) - }), - &grammar.typecodes(), - true, - nset, - ) - .map_err(|e| format!("Could not parse formula (GF): {}", e)) + grammar + .parse_formula( + &mut tokens.map(|t| { + Ok(FormulaToken { + symbol: nset.get_atom(&t), + span: metamath_knife::Span::NULL, + }) + }), + &grammar.typecodes(), + true, + nset, + ) + .map_err(|e| format!("Could not parse formula (GF): {}", e)) } } @@ -135,7 +144,11 @@ impl ExpressionRenderer { match self { ExpressionRenderer::Ascii => { let s = format!("
{}
", formula.as_ref(database)); - Ok(if use_provables { s.replace("wff ", " |- ") } else { s }) + Ok(if use_provables { + s.replace("wff ", " |- ") + } else { + s + }) } ExpressionRenderer::Unicode(uni) => uni.render_formula(formula), #[cfg(feature = "sts")] diff --git a/src/sts.rs b/src/sts.rs index d449e0b..f68da9e 100644 --- a/src/sts.rs +++ b/src/sts.rs @@ -132,7 +132,8 @@ impl StsDefinition { }; let mut mathml = self.format(typecode, formula)?; if !use_provables && typecode != grammar.provable_typecode() { - mathml = format!("{} {}", + mathml = format!( + "{} {}", as_str(self.database.name_result().atom_name(typecode)), self.format(formula.get_typecode(), formula)? );