implement registry wrapper

1 files changed, 8 insertions, 8 deletions

diff --git a/tools/Scanner/Parser.lean b/tools/Scanner/Parser.lean
index 7b64822..bb89648 100644
--- a/tools/Scanner/Parser.lean
+++ b/tools/Scanner/Parser.lean
@@ -44,16 +44,16 @@ private def Element.textContent (el : Xml.Element) : String :=
     |> String.intercalate "\n"
     |>.trimAscii
     |>.toString
-  reformat <| String.join <| Array.toList <| el.content.flatMap fun
-    | .Element _ => #[]
-    | .Comment _ => #[]
-    | .Character s => #[s]
+  reformat <| String.join <| Array.toList <| el.content.filterMap fun
+    | .Element _ => .none
+    | .Comment _ => .none
+    | .Character s => .some s
 
 private def Element.getChildrenByName (el : Xml.Element) (name : String) : Array Xml.Element :=
-  el.content.flatMap fun
-    | .Element child => if child.name == name then #[child] else #[]
-    | .Comment _ => #[]
-    | .Character _ => #[]
+  el.content.filterMap fun
+    | .Element child => if child.name == name then .some child else .none
+    | .Comment _ => .none
+    | .Character _ => .none
 
 private def Element.getChildByName (el : Xml.Element) (name : String) : Option Xml.Element :=
   match el.getChildrenByName name with