further cleanup

3 files changed, 50 insertions, 50 deletions

diff --git a/tools/Scanner.lean b/tools/Scanner.lean
index 1daed2a..17c30fd 100644
--- a/tools/Scanner.lean
+++ b/tools/Scanner.lean
@@ -56,5 +56,5 @@ def usage : IO UInt32 := do
 
 def main (args : List String) : IO UInt32 :=
   match args with
-  | [rootModule, outPath, srcPath] => process rootModule outPath srcPath
-  | _ => usage
+    | [rootModule, outPath, srcPath] => process rootModule outPath srcPath
+    | _ => usage
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"
diff --git a/tools/Scanner/Processor.lean b/tools/Scanner/Processor.lean
index 513d89f..a50767f 100644
--- a/tools/Scanner/Processor.lean
+++ b/tools/Scanner/Processor.lean
@@ -39,8 +39,8 @@ private def processEnumEntry (raw : Raw.EnumEntryDesc) : Processor Client.EnumEn
 
 private def interfaceInfo (name : String) : Processor InterfaceInfo := do
   match (← read).interfaces.get? name with
-  | .some info => pure info
-  | .none => .error s!"Unable to find referenced interface {name}"
+    | .some info => pure info
+    | .none => .error s!"Unable to find referenced interface {name}"
 
 private def resolveInterface (name : String) : TrackingProcessor Client.InterfaceRef := do
   let info ← interfaceInfo name
@@ -55,9 +55,9 @@ private def resolveInterface (name : String) : TrackingProcessor Client.Interfac
 private def resolveEnum (name : String) : Processor Client.EnumRef := do
   let (interface, enum) ←
     match (name.split ".").toArray with
-    | #[enum]            => pure ((← read).currentInterface.interface, enum.toString)
-    | #[interface, enum] => pure (interface.toString, enum.toString)
-    | _                  => throw s!"Malformed enum reference {name}"
+      | #[enum]            => pure ((← read).currentInterface.interface, enum.toString)
+      | #[interface, enum] => pure (interface.toString, enum.toString)
+      | _                  => throw s!"Malformed enum reference {name}"
   let info ← interfaceInfo interface
   if not (info.enums.contains enum) then
     throw s!"Interface {repr interface} does not contain enum {repr enum}"
@@ -81,14 +81,14 @@ private def processArgument (raw : Raw.ArgumentDesc) : TrackingProcessor Client.
     name := raw.name
     type :=
       ← match raw.type with
-      | .int    => Client.ArgumentType.int <$> raw.enum.mapM (liftM ∘ resolveEnum)
-      | .uint   => Client.ArgumentType.uint <$> raw.enum.mapM (liftM ∘ resolveEnum)
-      | .fixed  => Client.ArgumentType.fixed |> pure
-      | .string => Client.ArgumentType.string (.ofAllowNull raw.allowNull) |> pure
-      | .array  => Client.ArgumentType.array |> pure
-      | .fd     => Client.ArgumentType.fd |> pure
-      | .newID  => Client.ArgumentType.object .notNull <$> raw.interface.mapM resolveInterface
-      | .object => Client.ArgumentType.object (.ofAllowNull raw.allowNull) <$> raw.interface.mapM resolveInterface
+        | .int    => Client.ArgumentType.int <$> raw.enum.mapM (liftM ∘ resolveEnum)
+        | .uint   => Client.ArgumentType.uint <$> raw.enum.mapM (liftM ∘ resolveEnum)
+        | .fixed  => Client.ArgumentType.fixed |> pure
+        | .string => Client.ArgumentType.string (.ofAllowNull raw.allowNull) |> pure
+        | .array  => Client.ArgumentType.array |> pure
+        | .fd     => Client.ArgumentType.fd |> pure
+        | .newID  => Client.ArgumentType.object .notNull <$> raw.interface.mapM resolveInterface
+        | .object => Client.ArgumentType.object (.ofAllowNull raw.allowNull) <$> raw.interface.mapM resolveInterface
     description := raw.description
   }
 
@@ -97,9 +97,9 @@ private def processRequest (raw : Raw.MessageDesc) : TrackingProcessor Client.Re
   let otherArgs := raw.arguments.filter fun arg ↦ arg.type != .newID
   let returnType ←
     match newIDArgs with
-    | #[]    => Client.ReturnType.unit |> pure
-    | #[arg] => Client.ReturnType.object <$> arg.interface.mapM resolveInterface
-    | _      => throw s!"Expected at most one new_id argument for request in {raw.name}"
+      | #[]    => Client.ReturnType.unit |> pure
+      | #[arg] => Client.ReturnType.object <$> arg.interface.mapM resolveInterface
+      | _      => throw s!"Expected at most one new_id argument for request in {raw.name}"
   return {
     name := raw.name
     opcode := raw.opcode
@@ -158,11 +158,11 @@ private partial def transitiveClosure (protocols : Array Client.ProtocolDesc) :
     fun protocol ↦ protocol.interfaces.map
       fun iface ↦ ((⟨protocol.name, iface.name⟩ : Client.InterfaceRef), iface.referencedInterfaces.toList)
   let rec dfs : Std.TreeSet Client.InterfaceRef → List Client.InterfaceRef → Std.TreeSet Client.InterfaceRef
-  | visited, [] => visited
-  | visited, (x::xs) =>
-    if visited.contains x
-    then dfs visited xs
-    else dfs (visited.insert x) (successors.get! x ++ xs)
+    | visited, [] => visited
+    | visited, (x::xs) =>
+      if visited.contains x
+      then dfs visited xs
+      else dfs (visited.insert x) (successors.get! x ++ xs)
   let interfaceClosure (iface : Client.InterfaceDesc) : Client.InterfaceDesc :=
     { iface with referencedInterfaces := dfs .empty iface.referencedInterfaces.toList }
   let protocolClosure (protocol : Client.ProtocolDesc) : Client.ProtocolDesc :=