From 80d7f04bd73cdcf777afc0e2bb749f0be21cb896 Mon Sep 17 00:00:00 2001 From: Thierry Arnoux <5831830+tirix@users.noreply.github.com> Date: Sun, 12 Nov 2023 13:56:39 +0100 Subject: [PATCH 1/2] Correct STS typecode for syntax definitions --- src/statement.rs | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/src/statement.rs b/src/statement.rs index e4a6d15..bb1e49e 100644 --- a/src/statement.rs +++ b/src/statement.rs @@ -118,7 +118,7 @@ impl ExpressionRenderer { let nset = database.name_result(); let grammar = database.grammar_result(); let mut tokens = sref.math_iter(); - let _typecode = nset.get_atom(&tokens.next().unwrap()); + let typecode = nset.get_atom(&tokens.next().unwrap()); grammar .parse_formula( &mut tokens.map(|t| { @@ -128,7 +128,7 @@ impl ExpressionRenderer { }) }), &grammar.typecodes(), - true, + typecode == grammar.provable_typecode(), nset, ) .map_err(|e| format!("Could not parse formula (GF): {}", e)) @@ -143,12 +143,7 @@ impl ExpressionRenderer { ) -> Result { match self { ExpressionRenderer::Ascii => { - let s = format!("
{}
", formula.as_ref(database)); - Ok(if use_provables { - s.replace("wff ", " |- ") - } else { - s - }) + Ok(format!("
{}
", formula.as_ref(database))) } ExpressionRenderer::Unicode(uni) => uni.render_formula(formula), #[cfg(feature = "sts")] From bf8f09b7afd6392033307bcc781243d20d1f5019 Mon Sep 17 00:00:00 2001 From: Thierry Arnoux <5831830+tirix@users.noreply.github.com> Date: Sun, 12 Nov 2023 13:57:52 +0100 Subject: [PATCH 2/2] Fmt --- src/statement.rs | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/statement.rs b/src/statement.rs index bb1e49e..8baf0fc 100644 --- a/src/statement.rs +++ b/src/statement.rs @@ -139,12 +139,10 @@ impl ExpressionRenderer { &self, formula: &Formula, database: &Database, - use_provables: bool, + #[allow(unused_variables)] use_provables: bool, ) -> Result { match self { - ExpressionRenderer::Ascii => { - Ok(format!("
{}
", formula.as_ref(database))) - } + ExpressionRenderer::Ascii => Ok(format!("
{}
", formula.as_ref(database))), ExpressionRenderer::Unicode(uni) => uni.render_formula(formula), #[cfg(feature = "sts")] ExpressionRenderer::Sts(sts) => sts.render_formula(formula, use_provables),