@@ -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
668687end
669688
689+ def versoTextLine (allowNewlines := true ) : ParserFn := many1Fn (inline { allowNewlines })
690+
670691open Lean.Parser Term in
671692def 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
@@ -988,7 +1009,7 @@ open Lean Elab Term
9881009
9891010public def stringToInlines [Monad m] [MonadFileMap m] [MonadError m] [MonadEnv m] [MonadQuotation m] (s : StrLit) : m (Array Syntax) :=
9901011 withRef s do
991- return (← parseMarkupStrLit textLine s).getArgs
1012+ return (← parseMarkupStrLit versoTextLine s).getArgs
9921013
9931014open Lean Elab Term in
9941015public def stringToBlocks [Monad m] [MonadFileMap m] [MonadError m] [MonadEnv m] [MonadQuotation m] (s : StrLit) : m (Array Syntax) :=
0 commit comments