From dab858e92dfa5705d1aef7259e03b25747372d95 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Fri, 10 Apr 2026 17:36:15 +0200 Subject: implement registry wrapper --- tools/Scanner/Parser.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'tools/Scanner/Parser.lean') 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 -- cgit v1.3.1