fix: change same end maching

main
Xubai Wang 2022-02-20 05:03:44 +08:00
parent 794923a997
commit ad4d77a9c9
1 changed files with 19 additions and 22 deletions

View File

@ -3,13 +3,11 @@ import DocGen4.Output.Template
import Lean.Data.Parsec import Lean.Data.Parsec
import Unicode.General.GeneralCategory import Unicode.General.GeneralCategory
open Lean Unicode open Lean Unicode Xml Parser Parsec
namespace DocGen4 namespace DocGen4
namespace Output namespace Output
open Xml Parser Lean Parsec
instance : Inhabited Element := ⟨"", Std.RBMap.empty, #[]⟩ instance : Inhabited Element := ⟨"", Std.RBMap.empty, #[]⟩
/-- Parse an array of Xml/Html document from String. -/ /-- 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 def nameToLink? (s : String) : HtmlM (Option String) := do
let res ← getResult let res ← getResult
let name := s.splitOn "." |>.foldl (λ acc part => Name.mkStr acc part) Name.anonymous if let some name := Lean.Syntax.decodeNameLit ("`" ++ s) then
-- with exactly the same name -- with exactly the same name
if res.name2ModIdx.contains name then if res.name2ModIdx.contains name then
declNameToLink name declNameToLink name
-- find similar name in the same module -- find similar name in the same module
else else
match (← getCurrentName) with match (← getCurrentName) with
| some currentName => | some currentName =>
match (res.moduleInfo.find! currentName).members.find? (sameEnd ·.getName.toString s) with match res.moduleInfo.find! currentName |>.members |> filterMapDocInfo |>.find? (sameEnd ·.getName name) with
| some info => | some info =>
declNameToLink info.getName declNameToLink info.getName
| _ => pure none
| _ => pure none | _ => pure none
| _ => pure none else
pure none
where where
sameEnd n1 n2 := Id.run do -- check if two names have the same ending components
let n1' := n1.splitOn "." |>.reverse sameEnd n1 n2 :=
let n2' := n2.splitOn "." |>.reverse List.zip n1.components n2.components
for i in [0:n2'.length] do |>.all λ ⟨a, b⟩ => a == b
if n1'.getD i "" = n2'.get! i then
return true
return false
/-- /--
Extend links with following rules: Extend links with following rules: