From d43b23ec9ff69ff45956fa6ddb2a6eb2c4fbd699 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 11 Aug 2022 23:19:31 +0200
Subject: [PATCH] fix: Dont linkify unknown names

---
 DocGen4/Output/Base.lean | 26 +++++++++++++++-----------
 1 file changed, 15 insertions(+), 11 deletions(-)

diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index 2add29d..53ef5bc 100644
--- a/DocGen4/Output/Base.lean
+++ b/DocGen4/Output/Base.lean
@@ -212,17 +212,21 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
   | TaggedText.tag a t =>
     match a.info.val.info with
     | 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>]
-      | _ =>
+      let cleanExpr :=  i.expr.consumeMData
+      if let Expr.const name _ := cleanExpr then
+        -- TODO: this is some very primitive blacklisting but real Blacklisting needs MetaM
+        -- find a better solution
+        if (←getResult).name2ModIdx.contains name then
+          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]
+          | _ =>
+            pure #[<a href={←declNameToLink name}>[←infoFormatToHtml t]</a>]
+        else
+         pure #[<span class="fn">[←infoFormatToHtml t]</span>]
+      else
          pure #[<span class="fn">[←infoFormatToHtml t]</span>]
     | _ => pure #[<span class="fn">[←infoFormatToHtml t]</span>]