diff options
| author | Hannes Schulze <contact@haschu.me> | 2026-04-09 23:07:23 +0200 |
|---|---|---|
| committer | Hannes Schulze <contact@haschu.me> | 2026-04-09 23:07:23 +0200 |
| commit | 80317994ba8a8b7f72c0bf0d824e4ade59a4b6c8 (patch) | |
| tree | 9163cc9b663123acb2de6453ed50aa812b07f0b0 /lib/Wayland/Protocols/RiverInputManagementV1/Requests.lean | |
| parent | 924241fd20f582fe0935db960ed3f06a65920f6d (diff) | |
fix build on linux
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 |
