From 9550d1c92ea518463da25468df8dffeacbbff433 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Fri, 18 Feb 2022 03:26:38 +0800 Subject: [PATCH] refactor: use ## for intra doc --- DocGen4/Output/DocString.lean | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index f7005cf..70e6b0d 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -47,12 +47,15 @@ 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 - pure s + 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 pure s