diff options
Diffstat (limited to 'tools/Scanner')
| -rw-r--r-- | tools/Scanner/Parser.lean | 16 |
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 |