From d3d4cf3c160878758bdc17578c4d3055b1c80409 Mon Sep 17 00:00:00 2001
From: Khanh Le <nkgotcode@users.noreply.github.com>
Date: Thu, 18 Jun 2026 04:27:41 -0500
Subject: [PATCH] fix: parse parenthesized Markdown link URLs

---
 src/tests/Tests/Refs.lean   | 23 +++++++++++++++++++++++
 src/verso/Verso/Parser.lean | 33 +++++++++++++++++++++++++++------
 2 files changed, 50 insertions(+), 6 deletions(-)

diff --git a/src/tests/Tests/Refs.lean b/src/tests/Tests/Refs.lean
index 6da95723c..3dc828f11 100644
--- a/src/tests/Tests/Refs.lean
+++ b/src/tests/Tests/Refs.lean
@@ -27,6 +27,29 @@ info: Verso.Doc.Part.mk
   #eval regularLink.toPart
 
 
+/- ----- -/
+
+#docs (.none) parenthesizedUrlLink "Parenthesized URL link" :=
+:::::::
+Here is [a link](https://en.wikipedia.org/wiki/Function_(mathematics)).
+:::::::
+/--
+info: Verso.Doc.Part.mk
+  #[Verso.Doc.Inline.text "Parenthesized URL link"]
+  "Parenthesized URL link"
+  none
+  #[Verso.Doc.Block.para
+      #[Verso.Doc.Inline.text "Here is ",
+        Verso.Doc.Inline.link
+          #[(Verso.Doc.Inline.text "a link")]
+          "https://en.wikipedia.org/wiki/Function_(mathematics)",
+        Verso.Doc.Inline.text "."]]
+  #[]
+-/
+#guard_msgs in
+  #eval parenthesizedUrlLink.toPart
+
+
 /- ----- -/
 
 #docs (.none) refLink "Ref link" :=
diff --git a/src/verso/Verso/Parser.lean b/src/verso/Verso/Parser.lean
index 8db99208b..64f29db0b 100644
--- a/src/verso/Verso/Parser.lean
+++ b/src/verso/Verso/Parser.lean
@@ -626,7 +626,26 @@ mutual
 
   partial def linkTarget := ref <|> url
   where
-    notUrlEnd := satisfyEscFn (· ∉ ")\n".toList) "not ')' or newline" >> takeUntilEscFn (· ∈ ")\n".toList)
+    notUrlEnd := takeUrlTarget 0 false
+    takeUrlTarget (depth : Nat) (seen : Bool) : ParserFn := fun c s =>
+      let i := s.pos
+      if h : c.atEnd i then s
+      else
+        match c.get' i h with
+        | '\\' =>
+          let s := s.next' c i h
+          let i := s.pos
+          if h : c.atEnd i then s.mkEOIError
+          else takeUrlTarget depth true c (s.next' c i h)
+        | '\n' => s
+        | '(' => takeUrlTarget (depth + 1) true c (s.next' c i h)
+        | ')' =>
+          match depth with
+          | 0 =>
+            if seen then s
+            else s.mkUnexpectedError "not ')' or newline"
+          | depth' + 1 => takeUrlTarget depth' true c (s.next' c i h)
+        | _ => takeUrlTarget depth true c (s.next' c i h)
     notRefEnd := satisfyEscFn (· ∉ "]\n".toList) "not ']' or newline" >> takeUntilEscFn (· ∈ "]\n".toList)
     ref : ParserFn :=
       nodeFn ``Lean.Doc.Syntax.ref <|
@@ -667,6 +686,8 @@ mutual
     text <|> linebreak ctxt <|> delimitedInline ctxt
 end
 
+def versoTextLine (allowNewlines := true) : ParserFn := many1Fn (inline { allowNewlines })
+
 open Lean.Parser Term in
 def metadataContents : Parser :=
   structInstFields (sepByIndent structInstField ", " (allowTrailingSep := true))
@@ -772,7 +793,7 @@ mutual
   partial def descItem (ctxt : BlockCtxt) : ParserFn :=
     nodeFn ``desc <|
       colonFn >>
-      withCurrentColumn fun c => textLine >> ignoreFn (manyFn blankLine) >>
+      withCurrentColumn fun c => versoTextLine >> ignoreFn (manyFn blankLine) >>
       fakeAtom "=>" >>
       takeWhileFn (· == ' ') >>
       recoverSkip (guardColumn (· ≥ c) s!"indentation at least {c}" >>
@@ -817,7 +838,7 @@ mutual
     nodeFn ``para <|
       atomicFn (takeWhileFn (· == ' ') >> notFollowedByFn blockOpener "block opener" >> guardMinColumn ctxt.minIndent) >>
       withInfoSyntaxFn skip.fn (fun info => fakeAtom "para{" (info := info)) >>
-      textLine >>
+      versoTextLine >>
       withInfoSyntaxFn skip.fn (fun info => fakeAtom "}" (info := info))
 
   partial def header (ctxt : BlockCtxt) : ParserFn :=
@@ -831,7 +852,7 @@ mutual
             (show ParserFn from fun _ s => s.pushSyntax <| Syntax.mkNumLit (toString <| c' - c - 1)) >>
             fakeAtom ")") >>
       fakeAtom "{" >>
-      textLine (allowNewlines := false) >>
+      versoTextLine (allowNewlines := false) >>
       fakeAtom "}"
 
   partial def codeBlock (ctxt : BlockCtxt) : ParserFn :=
@@ -967,7 +988,7 @@ mutual
     nodeFn ``footnote_ref <|
       atomicFn (ignoreFn (bol >> eatSpaces >> guardMinColumn c.minIndent) >> strFn "[^" >> nodeFn strLitKind (asStringFn (quoted := true) (many1Fn (satisfyEscFn (· != ']') "not ']'"))) >> strFn "]:") >>
       eatSpaces >>
-      notFollowedByFn blockOpener "block opener" >> guardMinColumn c.minIndent >> textLine
+      notFollowedByFn blockOpener "block opener" >> guardMinColumn c.minIndent >> versoTextLine
 
   partial def block (c : BlockCtxt) : ParserFn :=
     block_command c <|> unorderedList c <|> orderedList c <|> definitionList c <|> header c <|> codeBlock c <|> directive c <|> blockquote c <|> linkRef c <|> footnoteRef c <|> para c <|> metadataBlock
@@ -988,7 +1009,7 @@ open Lean Elab Term
 
 public def stringToInlines [Monad m] [MonadFileMap m] [MonadError m] [MonadEnv m] [MonadQuotation m] (s : StrLit) : m (Array Syntax) :=
   withRef s do
-    return (← parseMarkupStrLit textLine s).getArgs
+    return (← parseMarkupStrLit versoTextLine s).getArgs
 
 open Lean Elab Term in
 public def stringToBlocks [Monad m] [MonadFileMap m] [MonadError m] [MonadEnv m] [MonadQuotation m] (s : StrLit) : m (Array Syntax) :=