1 files changed, 27 insertions, 27 deletions
diff --git a/tools/Scanner/Parser.lean b/tools/Scanner/Parser.lean
index 5d4e837..efe09bd 100644
--- a/tools/Scanner/Parser.lean
+++ b/tools/Scanner/Parser.lean
@@ -10,24 +10,24 @@ This converts a protocol description XML into a `Raw.ProtocolDesc`.
 
 private def String.toNat (s : String) : Except String Nat :=
   match Lean.Syntax.decodeNatLitVal? s with
-  | .some n => .ok n
-  | .none => .error s!"Expected a natural number, but got {s}"
+    | .some n => .ok n
+    | .none => .error s!"Expected a natural number, but got {s}"
 
 private def String.toBool : String → Except String Bool
-| "true" => .ok true
-| "false" => .ok false
-| s => .error s!"Expected a boolean value, but got {s}"
+  | "true" => .ok true
+  | "false" => .ok false
+  | s => .error s!"Expected a boolean value, but got {s}"
 
 namespace Lean.Xml
 
 private def Element.name : Xml.Element → String
-| .Element name _ _ => name
+  | .Element name _ _ => name
 
 private def Element.attributes : Xml.Element → Xml.Attributes
-| .Element _ attrs _ => attrs
+  | .Element _ attrs _ => attrs
 
 private def Element.content : Xml.Element → Array Xml.Content
-| .Element _ _ content => content
+  | .Element _ _ content => content
 
 private def Element.ensureName (el : Xml.Element) (name : String) : Except String Unit :=
   if name == el.name
@@ -45,20 +45,20 @@ private def Element.textContent (el : Xml.Element) : String :=
     |>.trimAscii
     |>.toString
   reformat <| String.join <| Array.toList <| el.content.flatMap fun
-  | .Element _ => #[]
-  | .Comment _ => #[]
-  | .Character s => #[s]
+    | .Element _ => #[]
+    | .Comment _ => #[]
+    | .Character s => #[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 _ => #[]
+    | .Element child => if child.name == name then #[child] else #[]
+    | .Comment _ => #[]
+    | .Character _ => #[]
 
 private def Element.getChildByName (el : Xml.Element) (name : String) : Option Xml.Element :=
   match el.getChildrenByName name with
-  | #[single] => .some single
-  | _ => .none
+    | #[single] => .some single
+    | _ => .none
 
 private def Element.getAttribute (el : Xml.Element) (attr : String) : Option String :=
   el.attributes.get? attr
@@ -77,19 +77,19 @@ namespace WaylandScanner
 open Raw
 
 private def MessageType.ofString : String → Except String MessageType
-| "destructor" => .ok .destructor
-| s => .error s!"Expected \"destructor\", but got {s}"
+  | "destructor" => .ok .destructor
+  | s => .error s!"Expected \"destructor\", but got {s}"
 
 private def ArgumentType.ofString : String → Except String ArgumentType
-| "int" => .ok .int
-| "uint" => .ok .uint
-| "fixed" => .ok .fixed
-| "string" => .ok .string
-| "array" => .ok .array
-| "fd" => .ok .fd
-| "new_id" => .ok .newID
-| "object" => .ok .object
-| s => .error s!"Expected an argument type, but got {s}"
+  | "int" => .ok .int
+  | "uint" => .ok .uint
+  | "fixed" => .ok .fixed
+  | "string" => .ok .string
+  | "array" => .ok .array
+  | "fd" => .ok .fd
+  | "new_id" => .ok .newID
+  | "object" => .ok .object
+  | s => .error s!"Expected an argument type, but got {s}"
 
 private def processDescription (el : Xml.Element) : Except String Description := do
   el.ensureName "description"