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 --- .../RiverInputManagementV1/Interface.lean | 142 +++++++++++++++++++++ 1 file changed, 142 insertions(+) create mode 100644 lib/Wayland/Protocols/RiverInputManagementV1/Interface.lean (limited to 'lib/Wayland/Protocols/RiverInputManagementV1/Interface.lean') diff --git a/lib/Wayland/Protocols/RiverInputManagementV1/Interface.lean b/lib/Wayland/Protocols/RiverInputManagementV1/Interface.lean new file mode 100644 index 0000000..7b72050 --- /dev/null +++ b/lib/Wayland/Protocols/RiverInputManagementV1/Interface.lean @@ -0,0 +1,142 @@ +import Wayland.Display +import Wayland.Protocols.RiverInputManagementV1.Header + +namespace Wayland.Protocols + +inductive RiverInputManagerV1.Event where + | finished + | inputDevice + (id : RiverInputDeviceV1) + +inductive RiverInputDeviceV1.Event where + | removed + | type + (type : RiverInputDeviceV1.Type) + | name + (name : String) + + +instance instInterfaceRiverInputManagerV1 : Interface RiverInputManagerV1.name where + event := RiverInputManagerV1.Event + version := 1 + requests := #[ + { + name := "stop" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "create_seat" + args := #[.string .notNull] + since := 1 + isDestructor := false + }, + { + name := "destroy_seat" + args := #[.string .notNull] + since := 1 + isDestructor := false + }, + ] + events := #[ + { + name := "finished" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "input_device" + args := #[.newID (.some "river_input_device_v1")] + since := 1 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .finished + | 1 => do + return .inputDevice + (← Marshallable.demarshal .object) + | _ => throw s!"Received invalid opcode" + +instance instInterfaceRiverInputDeviceV1 : Interface RiverInputDeviceV1.name where + event := RiverInputDeviceV1.Event + version := 1 + requests := #[ + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "assign_to_seat" + args := #[.string .notNull] + since := 1 + isDestructor := false + }, + { + name := "set_repeat_info" + args := #[.int, .int] + since := 1 + isDestructor := false + }, + { + name := "set_scroll_factor" + args := #[.fixed] + since := 1 + isDestructor := false + }, + { + name := "map_to_output" + args := #[.object .nullable (.some "wl_output")] + since := 1 + isDestructor := false + }, + { + name := "map_to_rectangle" + args := #[.int, .int, .int, .int] + since := 1 + isDestructor := false + }, + ] + events := #[ + { + name := "removed" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "type" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "name" + args := #[.string .notNull] + since := 1 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .removed + | 1 => do + return .type + (← Marshallable.demarshal .uint) + | 2 => do + return .name + (← Marshallable.demarshal .string) + | _ => throw s!"Received invalid opcode" + +end Wayland.Protocols \ No newline at end of file -- cgit v1.3.1