From 83c7c29075d58c89e6aa12acbc8823fbb2a4d7c5 Mon Sep 17 00:00:00 2001
From: kuruczgy <57020850+kuruczgy@users.noreply.github.com>
Date: Wed, 4 Oct 2023 02:51:22 +0200
Subject: [PATCH] fix: XML parsing bugs (#2601)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* 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           |  4 ++--
 tests/lean/xmlParsing.lean              | 10 ++++++++++
 tests/lean/xmlParsing.lean.expected.out |  2 ++
 3 files changed, 14 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/xmlParsing.lean
 create mode 100644 tests/lean/xmlParsing.lean.expected.out

diff --git a/src/Lean/Data/Xml/Parser.lean b/src/Lean/Data/Xml/Parser.lean
index 8b8dd40f41..7b8d5b0a8f 100644
--- a/src/Lean/Data/Xml/Parser.lean
+++ b/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)
 
diff --git a/tests/lean/xmlParsing.lean b/tests/lean/xmlParsing.lean
new file mode 100644
index 0000000000..f0947cdaf5
--- /dev/null
+++ b/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>"
diff --git a/tests/lean/xmlParsing.lean.expected.out b/tests/lean/xmlParsing.lean.expected.out
new file mode 100644
index 0000000000..bede94e914
--- /dev/null
+++ b/tests/lean/xmlParsing.lean.expected.out
@@ -0,0 +1,2 @@
+ok: <a><b a="v"></b></a>
+ok: <a><!-- comment --></a>