From a3b6e6c2ea339b54673caa26b7de0c1d63914f32 Mon Sep 17 00:00:00 2001
From: Thierry Arnoux <5831830+tirix@users.noreply.github.com>
Date: Mon, 30 Oct 2023 11:47:04 +0100
Subject: [PATCH] Remove links for hypotheses

---
 src/statement.hbs   |  8 ++++----
 src/statement.rs    | 16 ++++++++++++++++
 static/metamath.css |  2 +-
 3 files changed, 21 insertions(+), 5 deletions(-)

diff --git a/src/statement.hbs b/src/statement.hbs
index a66293b..09e0a7d 100644
--- a/src/statement.hbs
+++ b/src/statement.hbs
@@ -31,7 +31,7 @@
 			</ul>
 		</nav>
 		<hr />
-		<h2>{{statement_type}} <span class="label">{{label}}</span></h2>
+		<h2>{{statement_type}} <a href="#" class="label {{type}}">{{label}}</a></h2>
 		<p><strong>Description:</strong> {{comment}}</p>
 
 		<section class="statement">
@@ -46,14 +46,14 @@
 					<tr>
 						<td class="col-step"></td>
 						<td class="col-hyp">{{#if @first}}{{#if @last}}Hypothesis{{else}}Hypotheses{{/if}}{{/if}}</td>
-						<td class="col-ref" ><a href="{{label}}" class="label">{{label}}</a></td>
+						<td class="col-ref"><span class="hyp label">{{label}}</span></td>
 						<td class="col-expr">{{expr}}</td>
 					</tr>
 				{{/each}}
 				<tr>
 					<td class="col-step"></td>
 					<td class="col-hyp">Assertion</td>
-					<td class="col-ref" ><span class="label">{{label}}</span></td>
+					<td class="col-ref" ><a href="#" class="label {{type}}">{{label}}</a></td>
 					<td class="col-expr">{{expr}}</td>
 				</tr>
 			</table>
@@ -76,7 +76,7 @@
 							<td class="col-hyp">
 								{{#each hyps }}<a class="step" href="#{{this}}">{{this}}</a>{{#if (not @last)}} {{/if}}{{/each}}
 							</td>
-							<td class="col-ref" ><a href="{{label}}" class="label">{{label}}</a></td>
+							<td class="col-ref" >{{#if link}}<a href="{{label}}" class="label {{type}}">{{label}}</a>{{else}}<span class="label {{type}}">{{label}}</span>{{/if}}</td>
 							<td class="col-expr"><a name="{{id}}"></a>{{expr}}</td>
 						</tr>
 					{{/each}}
diff --git a/src/statement.rs b/src/statement.rs
index 4298321..f2aa29e 100644
--- a/src/statement.rs
+++ b/src/statement.rs
@@ -28,6 +28,8 @@ struct StepInfo {
     hyps: Vec<String>,
     label: String,
     expr: String,
+    r#type: String,
+    link: bool,
 }
 
 #[derive(Serialize)]
@@ -250,6 +252,16 @@ impl Renderer {
         ]
     }
 
+    fn stmt_type(stmt: StatementRef) -> String {
+        match stmt.statement_type() {
+            StatementType::Provable => "theorem".to_string(),
+            StatementType::Axiom => "axiom".to_string(),
+            StatementType::Essential => "hyp".to_string(),
+            StatementType::Floating => "float".to_string(),
+            _ => "other".to_string(),
+        }
+    }
+
     pub(crate) fn render_comment(&self, comment: &str) -> String {
         let comment = comment.replace("\n\n", "</p>\n<p>");
         let comment = self.contrib_regex.replace_all(&comment, |caps: &Captures| {
@@ -426,6 +438,8 @@ impl Renderer {
                             id: ix.to_string(),
                             hyps: hyps.iter().map(usize::to_string).collect::<Vec<String>>(),
                             label: as_str(stmt.label()).to_string(),
+                            r#type: Renderer::stmt_type(stmt),
+                            link: stmt.is_assertion(),
                             expr: expression_renderer
                                 .clone()
                                 .render_expression(&proof_tree, cur, true)
@@ -450,6 +464,8 @@ impl Renderer {
                             id: cur.to_string(),
                             hyps: hyps.iter().map(usize::to_string).collect::<Vec<String>>(),
                             label: as_str(stmt.label()).to_string(),
+                            r#type: Renderer::stmt_type(stmt),
+                            link: stmt.is_assertion(),
                             expr: expression_renderer
                                 .clone()
                                 .render_expression(&proof_tree, cur, false)
diff --git a/static/metamath.css b/static/metamath.css
index 5438aa4..3c754fd 100644
--- a/static/metamath.css
+++ b/static/metamath.css
@@ -87,7 +87,7 @@ table {
     background-color: #DEF;
 }
 
-.step {
+.step, .hyp.label {
     background-color: #EEE;
 }