From 80317994ba8a8b7f72c0bf0d824e4ade59a4b6c8 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Thu, 9 Apr 2026 23:07:23 +0200 Subject: fix build on linux --- .../Protocols/RiverInputManagementV1/Requests.lean | 91 ++++++++++++++++++++++ 1 file changed, 91 insertions(+) create mode 100644 lib/Wayland/Protocols/RiverInputManagementV1/Requests.lean (limited to 'lib/Wayland/Protocols/RiverInputManagementV1/Requests.lean') 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 -- cgit v1.3.1