fix: XML parsing bugs (#2601)

* fix: make XML parser handle trailing whitespace in opening tags

* fix: make XML parser handle comments correctly

---------

Co-authored-by: György Kurucz <me@kuruczgy.com>

src/Lean/Data/Xml/Parser.lean

@@ -119,7 +119,7 @@ def XMLdecl : Parsec Unit := do
 def Comment : Parsec String :=
   let notDash := Char.toString <$> satisfy (λ c => c ≠ '-')
   skipString "<!--" *>
-  Array.foldl String.append "" <$> many (notDash <|> (do
+  Array.foldl String.append "" <$> many (attempt <| notDash <|> (do
     let d ← pchar '-'
     let c ← notDash
     pure $ d.toString ++ c))
@@ -408,7 +408,7 @@ def Attribute : Parsec (String × String) := do
 protected def elementPrefix : Parsec (Array Content → Element) := do
   skipChar '<'
   let name ← Name
-  let attributes ← many (S *> Attribute)
+  let attributes ← many (attempt <| S *> Attribute)
   optional S *> pure ()
   return Element.Element name (RBMap.fromList attributes.toList compare)
 

tests/lean/xmlParsing.lean

@@ -0,0 +1,10 @@
+import Lean.Data.Xml
+open Lean.Xml
+
+/-! Test XML parsing. -/
+
+/-! Test whether trailing whitespace in opening tags is handled correctly. -/
+#eval parse "<a ><b a=\"v\" ></b></a>"
+
+/-! Test whether comments are parsed correctly. -/
+#eval parse "<a><!-- comment --></a>"

tests/lean/xmlParsing.lean.expected.out

@@ -0,0 +1,2 @@
+ok: <a><b a="v"></b></a>
+ok: <a><!-- comment --></a>