fix: remove intra link in code block
parent
11bb2af57a
commit
0b9a9f0bdc
|
@ -33,8 +33,10 @@ def textToIdAttribute (s : String) : String :=
|
||||||
def possibleNameToLink (s : String) : HtmlM (Option String) := do
|
def possibleNameToLink (s : String) : HtmlM (Option String) := do
|
||||||
let res ← getResult
|
let res ← getResult
|
||||||
let name := s.splitOn "." |>.foldl (λ acc part => Name.mkStr acc part) Name.anonymous
|
let name := s.splitOn "." |>.foldl (λ acc part => Name.mkStr acc part) Name.anonymous
|
||||||
|
-- with exactly the same name
|
||||||
if res.name2ModIdx.contains name then
|
if res.name2ModIdx.contains name then
|
||||||
declNameToLink name
|
declNameToLink name
|
||||||
|
-- find similar name in the same module
|
||||||
else
|
else
|
||||||
match (← getCurrentName) with
|
match (← getCurrentName) with
|
||||||
| some currentName =>
|
| some currentName =>
|
||||||
|
@ -52,7 +54,7 @@ def extendRelativeLink (s : String) : HtmlM String := do
|
||||||
else
|
else
|
||||||
pure s
|
pure s
|
||||||
-- for absolute and relative urls
|
-- for absolute and relative urls
|
||||||
else if s.startsWith "http" then
|
else if s.startsWith "http" then
|
||||||
pure s
|
pure s
|
||||||
else pure ((←getRoot) ++ s)
|
else pure ((←getRoot) ++ s)
|
||||||
|
|
||||||
|
@ -93,7 +95,7 @@ partial def modifyElement (element : Element) (linkCode : Bool := true) : HtmlM
|
||||||
| none => pure attrs
|
| none => pure attrs
|
||||||
pure ⟨ name, newAttrs, contents⟩
|
pure ⟨ name, newAttrs, contents⟩
|
||||||
-- auto link for inline <code></code>
|
-- auto link for inline <code></code>
|
||||||
else if name = "code" then
|
else if name = "code" ∧ linkCode then
|
||||||
let mut newContents := #[]
|
let mut newContents := #[]
|
||||||
for c in contents do
|
for c in contents do
|
||||||
match c with
|
match c with
|
||||||
|
|
Loading…
Reference in New Issue