refactor: use ## for intra doc
parent
89f5951f2d
commit
9550d1c92e
|
@ -47,11 +47,14 @@ def possibleNameToLink (s : String) : HtmlM (Option String) := do
|
|||
| _ => pure none
|
||||
|
||||
def extendRelativeLink (s : String) : HtmlM String := do
|
||||
-- for relative doc links
|
||||
if s.startsWith "#" then
|
||||
if let some link ← possibleNameToLink (s.drop 1) then
|
||||
-- for intra doc links
|
||||
if s.startsWith "##" then
|
||||
if let some link ← possibleNameToLink (s.drop 2) then
|
||||
pure link
|
||||
else
|
||||
panic! s!"Cannot find {s.drop 2}, only full name and abbrev in current module is supported"
|
||||
-- for id
|
||||
else if s.startsWith "#" then
|
||||
pure s
|
||||
-- for absolute and relative urls
|
||||
else if s.startsWith "http" then
|
||||
|
|
Loading…
Reference in New Issue