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>