From 19568c0659e55d9b96c712ac62c1983e65fd60a5 Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Wed, 13 Sep 2023 21:56:04 +0200
Subject: [PATCH] feat: autolink references to files

---
 DocGen4/Output/DocString.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean
index 6fe77f4..9465603 100644
--- 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