From ad4d77a9c9b3f8ff4da0a8d640e25b68f1af41c1 Mon Sep 17 00:00:00 2001
From: Xubai Wang <self@xubai.wang>
Date: Sun, 20 Feb 2022 05:03:44 +0800
Subject: [PATCH] fix: change same end maching

---
 DocGen4/Output/DocString.lean | 41 ++++++++++++++++-------------------
 1 file changed, 19 insertions(+), 22 deletions(-)

diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean
index 4470c54..7e8ae54 100644
--- a/DocGen4/Output/DocString.lean
+++ b/DocGen4/Output/DocString.lean
@@ -3,13 +3,11 @@ import DocGen4.Output.Template
 import Lean.Data.Parsec
 import Unicode.General.GeneralCategory
 
-open Lean Unicode
+open Lean Unicode  Xml Parser Parsec
 
 namespace DocGen4
 namespace Output
 
-open Xml Parser Lean Parsec
-
 instance : Inhabited Element := ⟨"", Std.RBMap.empty, #[]⟩
 
 /-- Parse an array of Xml/Html document from String. -/
@@ -51,27 +49,26 @@ partial def xmlGetHeadingId (el : Xml.Element) : String :=
 -/
 def nameToLink? (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 =>
-      match (res.moduleInfo.find! currentName).members.find? (sameEnd ·.getName.toString s) with
-      | some info => 
-        declNameToLink info.getName
+  if let some name := Lean.Syntax.decodeNameLit ("`" ++ s) then
+    -- 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 =>
+        match res.moduleInfo.find! currentName |>.members |> filterMapDocInfo |>.find? (sameEnd ·.getName name) with
+        | some info => 
+          declNameToLink info.getName
+        | _ => pure none
       | _ => pure none
-    | _ => pure none
+  else
+    pure none
   where
-    sameEnd n1 n2 := Id.run do
-      let n1' := n1.splitOn "." |>.reverse
-      let n2' := n2.splitOn "." |>.reverse
-      for i in [0:n2'.length] do
-        if n1'.getD i "" = n2'.get! i then
-          return true
-      return false
+    -- check if two names have the same ending components
+    sameEnd n1 n2 :=
+      List.zip n1.components n2.components
+      |>.all λ ⟨a, b⟩ => a == b
 
 /--
   Extend links with following rules: