Skip to content

Commit 32ff87e

Browse files
committed
fix: parse parenthesized Markdown link URLs
1 parent b677415 commit 32ff87e

2 files changed

Lines changed: 50 additions & 6 deletions

File tree

src/tests/Tests/Refs.lean

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,29 @@ info: Verso.Doc.Part.mk
2727
#eval regularLink.toPart
2828

2929

30+
/- ----- -/
31+
32+
#docs (.none) parenthesizedUrlLink "Parenthesized URL link" :=
33+
:::::::
34+
Here is [a link](https://en.wikipedia.org/wiki/Function_(mathematics)).
35+
:::::::
36+
/--
37+
info: Verso.Doc.Part.mk
38+
#[Verso.Doc.Inline.text "Parenthesized URL link"]
39+
"Parenthesized URL link"
40+
none
41+
#[Verso.Doc.Block.para
42+
#[Verso.Doc.Inline.text "Here is ",
43+
Verso.Doc.Inline.link
44+
#[(Verso.Doc.Inline.text "a link")]
45+
"https://en.wikipedia.org/wiki/Function_(mathematics)",
46+
Verso.Doc.Inline.text "."]]
47+
#[]
48+
-/
49+
#guard_msgs in
50+
#eval parenthesizedUrlLink.toPart
51+
52+
3053
/- ----- -/
3154

3255
#docs (.none) refLink "Ref link" :=

src/verso/Verso/Parser.lean

Lines changed: 27 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -626,7 +626,26 @@ mutual
626626

627627
partial def linkTarget := ref <|> url
628628
where
629-
notUrlEnd := satisfyEscFn (· ∉ ")\n".toList) "not ')' or newline" >> takeUntilEscFn (· ∈ ")\n".toList)
629+
notUrlEnd := takeUrlTarget 0 false
630+
takeUrlTarget (depth : Nat) (seen : Bool) : ParserFn := fun c s =>
631+
let i := s.pos
632+
if h : c.atEnd i then s
633+
else
634+
match c.get' i h with
635+
| '\\' =>
636+
let s := s.next' c i h
637+
let i := s.pos
638+
if h : c.atEnd i then s.mkEOIError
639+
else takeUrlTarget depth true c (s.next' c i h)
640+
| '\n' => s
641+
| '(' => takeUrlTarget (depth + 1) true c (s.next' c i h)
642+
| ')' =>
643+
match depth with
644+
| 0 =>
645+
if seen then s
646+
else s.mkUnexpectedError "not ')' or newline"
647+
| depth' + 1 => takeUrlTarget depth' true c (s.next' c i h)
648+
| _ => takeUrlTarget depth true c (s.next' c i h)
630649
notRefEnd := satisfyEscFn (· ∉ "]\n".toList) "not ']' or newline" >> takeUntilEscFn (· ∈ "]\n".toList)
631650
ref : ParserFn :=
632651
nodeFn ``Lean.Doc.Syntax.ref <|
@@ -667,6 +686,8 @@ mutual
667686
text <|> linebreak ctxt <|> delimitedInline ctxt
668687
end
669688

689+
def versoTextLine (allowNewlines := true) : ParserFn := many1Fn (inline { allowNewlines })
690+
670691
open Lean.Parser Term in
671692
def metadataContents : Parser :=
672693
structInstFields (sepByIndent structInstField ", " (allowTrailingSep := true))
@@ -772,7 +793,7 @@ mutual
772793
partial def descItem (ctxt : BlockCtxt) : ParserFn :=
773794
nodeFn ``desc <|
774795
colonFn >>
775-
withCurrentColumn fun c => textLine >> ignoreFn (manyFn blankLine) >>
796+
withCurrentColumn fun c => versoTextLine >> ignoreFn (manyFn blankLine) >>
776797
fakeAtom "=>" >>
777798
takeWhileFn (· == ' ') >>
778799
recoverSkip (guardColumn (· ≥ c) s!"indentation at least {c}" >>
@@ -817,7 +838,7 @@ mutual
817838
nodeFn ``para <|
818839
atomicFn (takeWhileFn (· == ' ') >> notFollowedByFn blockOpener "block opener" >> guardMinColumn ctxt.minIndent) >>
819840
withInfoSyntaxFn skip.fn (fun info => fakeAtom "para{" (info := info)) >>
820-
textLine >>
841+
versoTextLine >>
821842
withInfoSyntaxFn skip.fn (fun info => fakeAtom "}" (info := info))
822843

823844
partial def header (ctxt : BlockCtxt) : ParserFn :=
@@ -831,7 +852,7 @@ mutual
831852
(show ParserFn from fun _ s => s.pushSyntax <| Syntax.mkNumLit (toString <| c' - c - 1)) >>
832853
fakeAtom ")") >>
833854
fakeAtom "{" >>
834-
textLine (allowNewlines := false) >>
855+
versoTextLine (allowNewlines := false) >>
835856
fakeAtom "}"
836857

837858
partial def codeBlock (ctxt : BlockCtxt) : ParserFn :=
@@ -967,7 +988,7 @@ mutual
967988
nodeFn ``footnote_ref <|
968989
atomicFn (ignoreFn (bol >> eatSpaces >> guardMinColumn c.minIndent) >> strFn "[^" >> nodeFn strLitKind (asStringFn (quoted := true) (many1Fn (satisfyEscFn (· != ']') "not ']'"))) >> strFn "]:") >>
969990
eatSpaces >>
970-
notFollowedByFn blockOpener "block opener" >> guardMinColumn c.minIndent >> textLine
991+
notFollowedByFn blockOpener "block opener" >> guardMinColumn c.minIndent >> versoTextLine
971992

972993
partial def block (c : BlockCtxt) : ParserFn :=
973994
block_command c <|> unorderedList c <|> orderedList c <|> definitionList c <|> header c <|> codeBlock c <|> directive c <|> blockquote c <|> linkRef c <|> footnoteRef c <|> para c <|> metadataBlock
@@ -987,7 +1008,7 @@ open Lean Elab Term
9871008

9881009
public def stringToInlines [Monad m] [MonadError m] [MonadEnv m] [MonadQuotation m] (s : StrLit) : m (Array Syntax) :=
9891010
withRef s do
990-
return (← textLine.parseString s.getString).getArgs
1011+
return (← versoTextLine.parseString s.getString).getArgs
9911012

9921013
open Lean Elab Term in
9931014
public def stringToBlocks [Monad m] [MonadError m] [MonadEnv m] [MonadQuotation m] (s : StrLit) : m (Array Syntax) :=

0 commit comments

Comments
 (0)