feat: autolink references to files

leanprover · Sep 16, 2023 · 19568c0 · 19568c0
1 parent f9b5a29
commit 19568c0
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean
@@ -70,7 +70,9 @@ partial def xmlGetHeadingId (el : Xml.Element) : String :=
 -/
 def nameToLink? (s : String) : HtmlM (Option String) := do
   let res ← getResult
-  if let some name := Lean.Syntax.decodeNameLit ("`" ++ s) then
+  if s.endsWith ".lean" && s.contains '/' then
+    return (← getRoot) ++ s.dropRight 5 ++ ".html"
+  else if let some name := Lean.Syntax.decodeNameLit ("`" ++ s) then
     -- with exactly the same name
     if res.name2ModIdx.contains name then
       declNameToLink name