From 0ac64f08738109c212394d134ddbc462673a9a76 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 26 Jul 2022 15:12:29 +0200
Subject: [PATCH] types, types everywhere

---
 DocGen4/LeanInk/Output.lean | 15 ++++++++++-----
 DocGen4/Output/Base.lean    | 16 ++++++++--------
 lean_packages/manifest.json |  2 +-
 3 files changed, 19 insertions(+), 14 deletions(-)

diff --git a/DocGen4/LeanInk/Output.lean b/DocGen4/LeanInk/Output.lean
index a01ce80..5c719b1 100644
--- a/DocGen4/LeanInk/Output.lean
+++ b/DocGen4/LeanInk/Output.lean
@@ -35,7 +35,7 @@ def TypeInfo.toHtml (tyi : TypeInfo) : AlectryonM Html := do
               <span class="hyp-type">
                 <var>{tyi.name}</var>
                 <b>: </b>
-                <span>{tyi.type}</span>
+                <span>[←DocGen4.Output.infoFormatToHtml tyi.type.fst]</span>
               </span>
             </div>
           </blockquote>
@@ -80,16 +80,16 @@ def Contents.toHtml : Contents → AlectryonM Html
 
 def Hypothesis.toHtml (h : Hypothesis) : AlectryonM Html := do
   let mut hypParts := #[<var>[h.names.intersperse ", " |>.map Html.text |>.toArray]</var>]
-  if h.body != "" then
+  if h.body.snd != "" then
     hypParts := hypParts.push
       <span class="hyp-body">
         <b>:= </b>
-        <span>{h.body}</span>
+        <span>[←infoFormatToHtml h.body.fst]</span>
       </span>
   hypParts := hypParts.push
       <span class="hyp-type">
         <b>: </b>
-        <span >{h.type}</span>
+        <span >[←infoFormatToHtml h.type.fst]</span>
       </span>
 
   pure
@@ -103,6 +103,11 @@ def Goal.toHtml (g : Goal) : AlectryonM Html := do
     let rendered ← hyp.toHtml
     hypotheses := hypotheses.push rendered
     hypotheses := hypotheses.push <br/>
+  let conclusionHtml ←
+    match g.conclusion with
+    | .typed info _ => infoFormatToHtml info
+    | .untyped str => pure <| #[Html.text str]
+
   pure
     <blockquote class="alectryon-goal">
       <div class="goal-hyps">
@@ -112,7 +117,7 @@ def Goal.toHtml (g : Goal) : AlectryonM Html := do
         <hr><span class="goal-name">{g.name}</span></hr>
       </span>
       <div class="goal-conclusion">
-        {g.conclusion}
+        [conclusionHtml]
       </div>
     </blockquote>
 
diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index 8fd2d7c..c2292d1 100644
--- a/DocGen4/Output/Base.lean
+++ b/DocGen4/Output/Base.lean
@@ -209,14 +209,14 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
     | Info.ofTermInfo i =>
       match i.expr.consumeMData with
       | Expr.const name _ =>
-         match t with
-         | TaggedText.text t =>
-           let (front, t, back) := splitWhitespaces <| Html.escape t
-           let elem := <a href={←declNameToLink name}>{t}</a>
-           pure #[Html.text front, elem, Html.text back]
-         | _ =>
-           -- TODO: Is this ever reachable?
-           pure #[<a href={←declNameToLink name}>[←infoFormatToHtml t]</a>]
+        match t with
+        | TaggedText.text t =>
+          let (front, t, back) := splitWhitespaces <| Html.escape t
+          let elem := <a href={←declNameToLink name}>{t}</a>
+          pure #[Html.text front, elem, Html.text back]
+        | _ =>
+          -- TODO: Is this ever reachable?
+          pure #[<a href={←declNameToLink name}>[←infoFormatToHtml t]</a>]
       | _ =>
          pure #[<span class="fn">[←infoFormatToHtml t]</span>]
     | _ => pure #[<span class="fn">[←infoFormatToHtml t]</span>]
diff --git a/lean_packages/manifest.json b/lean_packages/manifest.json
index ed6a9b1..c8924d6 100644
--- a/lean_packages/manifest.json
+++ b/lean_packages/manifest.json
@@ -4,7 +4,7 @@
    "rev": "112b35fc348a4a18d2111ac2c6586163330b4941",
    "name": "Cli"},
   {"url": "https://github.com/hargonix/LeanInk",
-   "rev": "3ab183e60a2aa082fb20c3bc139b992f683ae1d4",
+   "rev": "0c113bb4cc88d4b8dc6b2d26a4c4c9cf6008a2eb",
    "name": "leanInk"},
   {"url": "https://github.com/xubaiw/Unicode.lean",
    "rev": "1fb004da96aa1d1e98535951e100439a60f5b7f0",