From ed8d1c3e7e82d8548c028110445a22df74568a91 Mon Sep 17 00:00:00 2001
From: acmepjz <acme_pjz@hotmail.com>
Date: Mon, 8 Jul 2024 03:04:56 +0800
Subject: [PATCH] feat: use `find` instead of `panic` in `extendLink`

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

diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean
index 26d6c38e..05f9c738 100644
--- a/DocGen4/Output/DocString.lean
+++ b/DocGen4/Output/DocString.lean
@@ -99,7 +99,7 @@ def nameToLink? (s : String) : HtmlM (Option String) := do
 /--
   Extend links with following rules:
 
-  1. if the link starts with `##`, a name search is used and will panic if not found
+  1. if the link starts with `##`, a name search is used, and will use `find` if not found
   2. if the link starts with `#`, it's treated as id link, no modification
   3. if the link starts with `http`, it's an absolute one, no modification
   4. otherwise it's a relative link, extend it with base url
@@ -110,7 +110,7 @@ def extendLink (s : String)  : HtmlM String := do
     if let some link ← nameToLink? (s.drop 2) then
       return link
     else
-      panic! s!"Cannot find {s.drop 2}, only full name and abbrev in current module is supported"
+      return s!"{← getRoot}find/?pattern={s.drop 2}#doc"
   -- for id
   else if s.startsWith "#" then
     return s