diff options
Diffstat (limited to 'lib/Wayland/Protocols/RiverInputManagementV1/Requests.lean')
| -rw-r--r-- | lib/Wayland/Protocols/RiverInputManagementV1/Requests.lean | 91 |
1 files changed, 91 insertions, 0 deletions
diff --git a/lib/Wayland/Protocols/RiverInputManagementV1/Requests.lean b/lib/Wayland/Protocols/RiverInputManagementV1/Requests.lean new file mode 100644 index 0000000..3c9c44e --- /dev/null +++ b/lib/Wayland/Protocols/RiverInputManagementV1/Requests.lean @@ -0,0 +1,91 @@ +import Wayland.Display +import Wayland.Protocols.RiverInputManagementV1.Resolved +import Wayland.Protocols.Wayland.Header + +namespace Wayland.Protocols + +variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι] + +def RiverInputManagerV1.stop + (ω : RiverInputManagerV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverInputManagerV1.destroy + (ω : RiverInputManagerV1) + : DisplayM σ Unit := + ω.send do + return 1 + +def RiverInputManagerV1.createSeat + (ω : RiverInputManagerV1) + (name : String) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .string name + return 2 + +def RiverInputManagerV1.destroySeat + (ω : RiverInputManagerV1) + (name : String) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .string name + return 3 + +def RiverInputDeviceV1.destroy + (ω : RiverInputDeviceV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverInputDeviceV1.assignToSeat + (ω : RiverInputDeviceV1) + (name : String) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .string name + return 1 + +def RiverInputDeviceV1.setRepeatInfo + (ω : RiverInputDeviceV1) + (rate : Int32) + (delay : Int32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .int rate + Marshallable.marshal .int delay + return 2 + +def RiverInputDeviceV1.setScrollFactor + (ω : RiverInputDeviceV1) + (factor : Float32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .fixed factor + return 3 + +def RiverInputDeviceV1.mapToOutput + (ω : RiverInputDeviceV1) + (output : Option WlOutput) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object output + return 4 + +def RiverInputDeviceV1.mapToRectangle + (ω : RiverInputDeviceV1) + (x : Int32) + (y : Int32) + (width : Int32) + (height : Int32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .int x + Marshallable.marshal .int y + Marshallable.marshal .int width + Marshallable.marshal .int height + return 5 + +end Wayland.Protocols
\ No newline at end of file |
