From 0b9a9f0bdc96911996aa7f1ccf133e53d8a62287 Mon Sep 17 00:00:00 2001
From: Xubai Wang <self@xubai.wang>
Date: Fri, 18 Feb 2022 01:39:02 +0800
Subject: [PATCH] fix: remove intra link in code block

---
 DocGen4/Output/DocString.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean
index 66f5015..f7005cf 100644
--- a/DocGen4/Output/DocString.lean
+++ b/DocGen4/Output/DocString.lean
@@ -33,8 +33,10 @@ def textToIdAttribute (s : String) : String :=
 def possibleNameToLink (s : String) : HtmlM (Option String) := do
   let res ← getResult
   let name := s.splitOn "." |>.foldl (λ acc part => Name.mkStr acc part) Name.anonymous
+  -- with exactly the same name
   if res.name2ModIdx.contains name then
      declNameToLink name
+  -- find similar name in the same module
   else
     match (← getCurrentName) with
     | some currentName =>
@@ -52,7 +54,7 @@ def extendRelativeLink (s : String)  : HtmlM String := do
     else
       pure s
   -- for absolute and relative urls
-  else if s.startsWith "http" then
+  else if s.startsWith "http" then 
     pure s
   else pure ((←getRoot) ++ s)
 
@@ -93,7 +95,7 @@ partial def modifyElement (element : Element) (linkCode : Bool := true) : HtmlM
       | none => pure attrs
       pure ⟨ name, newAttrs, contents⟩
     -- auto link for inline <code></code>
-    else if name = "code" then
+    else if name = "code" ∧ linkCode then
       let mut newContents := #[]
       for c in contents do
         match c with