Skip to content

Commit

Permalink
feat: use find instead of panic in extendLink
Browse files Browse the repository at this point in the history
  • Loading branch information
acmepjz committed Jul 7, 2024
1 parent b5197b6 commit ed8d1c3
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions DocGen4/Output/DocString.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down

0 comments on commit ed8d1c3

Please sign in to comment.