From 3acfc510b45e1caeb851fb5ecd302a2cdc4a657b Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Sun, 20 Feb 2022 03:28:03 +0800 Subject: [PATCH] fix: no overmatch for intra link --- DocGen4/Output/DocString.lean | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index 7c933b0..4470c54 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -59,11 +59,19 @@ def nameToLink? (s : String) : HtmlM (Option String) := do else match (← getCurrentName) with | some currentName => - match (res.moduleInfo.find! currentName).members.find? (·.getName.toString.endsWith s) with + match (res.moduleInfo.find! currentName).members.find? (sameEnd ·.getName.toString s) with | some info => declNameToLink info.getName | _ => pure none | _ => 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 /-- Extend links with following rules: