diff options
| -rw-r--r-- | lib/CWayland/CWayland.cc | 445 | ||||
| -rw-r--r-- | lib/CWayland/CWayland.h | 24 | ||||
| -rw-r--r-- | lib/Wayland/Display.lean | 16 | ||||
| -rw-r--r-- | lib/Wayland/Native.lean | 64 |
4 files changed, 519 insertions, 30 deletions
diff --git a/lib/CWayland/CWayland.cc b/lib/CWayland/CWayland.cc index cf1687a..cff3fd1 100644 --- a/lib/CWayland/CWayland.cc +++ b/lib/CWayland/CWayland.cc @@ -40,7 +40,7 @@ namespace return ref{ ptr, steal_token{} }; } - explicit ref() : ptr{ nullptr } + ref() : ptr{ nullptr } { } @@ -122,6 +122,19 @@ namespace return lean_io_result_mk_error(error); } + + std::size_t message_argument_count(const wl_message* msg) + { + std::size_t res = 0; + for (char c : std::string_view{ msg->signature }) + { + if (c >= 'a' && c <= 'z') { res += 1; } + } + return res; + } + + // Global dispatcher func, assumes a user_data of type (UInt32 → ArgumentReader → EventLoop M × M) + int dispatcher_func(const void* user_data, void* target, uint32_t opcode, const wl_message* msg, wl_argument* args); } // -- Constants @@ -148,7 +161,15 @@ namespace lean_external_class* waylean_display_class() { static lean_external_class* klass = lean_register_external_class( - [](void* ptr) { wl_display_disconnect(static_cast<wl_display*>(ptr)); }, + [](void* ptr) + { + auto disp = static_cast<wl_display*>(ptr); + if (auto user_data = wl_proxy_get_user_data((wl_proxy*)disp)) + { + lean_dec(static_cast<lean_object*>(user_data)); + } + wl_display_disconnect(disp); + }, [](void*, b_lean_obj_arg fn) { } ); return klass; @@ -161,8 +182,10 @@ lean_obj_res waylean_display_new(b_lean_obj_arg name) char const* name_cstr = option_cstr_or_null(name); wl_display* disp = wl_display_connect(name_cstr); if (!disp) { return io_result_mk_from_errno(name_cstr ? name_cstr : "<default>"); } - lean_object* waylean_disp = lean_alloc_external(waylean_display_class(), disp); + + wl_proxy_add_dispatcher((wl_proxy*)disp, dispatcher_func, waylean_disp, nullptr); + return lean_io_result_mk_ok(waylean_disp); } @@ -320,6 +343,8 @@ namespace timer_source_queue timers; std::vector<pollfd> pollfds; std::deque<scheduled_event> scheduled; + // Display source ID currently in dispatch_pending, used to associate events with their source ID. + size_t dispatching_display{}; void rebuild_pollfds() { @@ -403,6 +428,14 @@ namespace return res; } + void queue_display_message(ref message) + { + auto ev = scheduled_event{}; + ev.id = dispatching_display; + ev.message = std::move(message); + scheduled.emplace_back(std::move(ev)); + } + void remove(event_source const& source) { // Discharge event source long-term. @@ -456,6 +489,7 @@ namespace // Otherwise, fetch any new events. for (auto& src : displays) { + dispatching_display = src.id; while (wl_display_prepare_read(src.disp)) { if (wl_display_dispatch_pending(src.disp) == -1) @@ -509,6 +543,7 @@ namespace // 2. Process display events. for (auto& src : displays) { + dispatching_display = src.id; if (wl_display_read_events(src.disp) == -1) { perror("event_loop::poll: wl_display_read_events"); @@ -810,24 +845,416 @@ lean_obj_res waylean_type_map_register(b_lean_obj_arg map_obj, b_lean_obj_arg if return lean_io_result_mk_ok(lean_box(0)); } +// -- Argument Writer + +namespace +{ + class argument_writer + { + static constexpr std::size_t max_args = 64; + + std::size_t used{ 0 }; + std::array<wl_argument, max_args> args{}; + std::array<ref, max_args> refs{}; + + std::size_t new_arg() + { + assert(used + 1 < max_args && "reached maximum number of arguments"); + return used++; + } + + public: + wl_argument* get_args() { return args.data(); } + + void write_int(int32_t value) + { + auto i = new_arg(); + args[i].i = value; + } + + void write_uint(uint32_t value) + { + auto i = new_arg(); + args[i].u = value; + } + + void write_fixed(float value) + { + auto i = new_arg(); + args[i].f = wl_fixed_from_double(value); + } + + void write_string(b_lean_obj_arg value) + { + auto i = new_arg(); + if (lean_is_scalar(value)) + { + args[i].s = nullptr; + } + else + { + lean_object* val = lean_ctor_get(value, 0); + args[i].s = lean_string_cstr(val); + refs[i] = ref{ val }; + } + } + + void write_object(b_lean_obj_arg value) + { + auto i = new_arg(); + if (lean_is_scalar(value)) + { + args[i].o = nullptr; + } + else + { + lean_object* val = lean_ctor_get(value, 0); + args[i].o = static_cast<wl_object*>(lean_get_external_data(val)); + refs[i] = ref{ val }; + } + } + + void write_new_id(b_lean_obj_arg value) + { + auto i = new_arg(); + args[i].n = wl_proxy_get_id(static_cast<wl_proxy*>(lean_get_external_data(value))); + refs[i] = ref{ value }; + } + + void write_array(b_lean_obj_arg value) + { + auto i = new_arg(); + std::size_t size = lean_sarray_size(value); + args[i].a->alloc = size; + args[i].a->size = size; + args[i].a->data = lean_sarray_cptr(value); + refs[i] = ref{ value }; + } + + void write_fd(int32_t value) + { + auto i = new_arg(); + args[i].h = value; + } + }; + + lean_external_class* waylean_argument_writer_class() + { + static lean_external_class* klass = lean_register_external_class( + [](void* ptr) { delete static_cast<argument_writer*>(ptr); }, + [](void*, b_lean_obj_arg fn) { } + ); + return klass; + } +} + +// ArgumentWriter.new : IO ArgumentWriter +lean_obj_res waylean_argument_writer_new(void) +{ + argument_writer* writer = new argument_writer; + lean_object* waylean_writer = lean_alloc_external(waylean_argument_writer_class(), writer); + return lean_io_result_mk_ok(waylean_writer); +} + +// ArgumentWriter.writeInt : (writer : @& ArgumentWriter) → (value : Int32) → IO Unit +lean_obj_res waylean_argument_writer_write_int(b_lean_obj_arg writer_obj, int32_t value) +{ + auto writer = static_cast<argument_writer*>(lean_get_external_data(writer_obj)); + writer->write_int(value); + return lean_io_result_mk_ok(lean_box(0)); +} + +// ArgumentWriter.writeUInt : (writer : @& ArgumentWriter) → (value : UInt32) → IO Unit +lean_obj_res waylean_argument_writer_write_uint(b_lean_obj_arg writer_obj, uint32_t value) +{ + auto writer = static_cast<argument_writer*>(lean_get_external_data(writer_obj)); + writer->write_uint(value); + return lean_io_result_mk_ok(lean_box(0)); +} + +// ArgumentWriter.writeFloat : (writer : @& ArgumentWriter) → (value : Float) → IO Unit +lean_obj_res waylean_argument_writer_write_fixed(b_lean_obj_arg writer_obj, float value) +{ + auto writer = static_cast<argument_writer*>(lean_get_external_data(writer_obj)); + writer->write_fixed(value); + return lean_io_result_mk_ok(lean_box(0)); +} + +// ArgumentWriter.writeString : (writer : @& ArgumentWriter) → (value : @& Option String) → IO Unit +lean_obj_res waylean_argument_writer_write_string(b_lean_obj_arg writer_obj, b_lean_obj_arg value) +{ + auto writer = static_cast<argument_writer*>(lean_get_external_data(writer_obj)); + writer->write_string(value); + return lean_io_result_mk_ok(lean_box(0)); +} + +// ArgumentWriter.writeObject : (writer : @& ArgumentWriter) → (value : @& Option Proxy) → IO Unit +lean_obj_res waylean_argument_writer_write_object(b_lean_obj_arg writer_obj, b_lean_obj_arg value) +{ + auto writer = static_cast<argument_writer*>(lean_get_external_data(writer_obj)); + writer->write_object(value); + return lean_io_result_mk_ok(lean_box(0)); +} + +// ArgumentWriter.writeNewID : (writer : @& ArgumentWriter) → (value : @& Proxy) → IO Unit +lean_obj_res waylean_argument_writer_write_new_id(b_lean_obj_arg writer_obj, b_lean_obj_arg value) +{ + auto writer = static_cast<argument_writer*>(lean_get_external_data(writer_obj)); + writer->write_new_id(value); + return lean_io_result_mk_ok(lean_box(0)); +} + +// ArgumentWriter.writeArray : (writer : @& ArgumentWriter) → (value : @& ByteArray) → IO Unit +lean_obj_res waylean_argument_writer_write_array(b_lean_obj_arg writer_obj, b_lean_obj_arg value) +{ + auto writer = static_cast<argument_writer*>(lean_get_external_data(writer_obj)); + writer->write_array(value); + return lean_io_result_mk_ok(lean_box(0)); +} + +// ArgumentWriter.writeFD : (writer : @& ArgumentWriter) → (value : Int32) → IO Unit +lean_obj_res waylean_argument_writer_write_fd(b_lean_obj_arg writer_obj, int32_t value) +{ + auto writer = static_cast<argument_writer*>(lean_get_external_data(writer_obj)); + writer->write_fd(value); + return lean_io_result_mk_ok(lean_box(0)); +} + +// -- Argument Reader + +namespace +{ + struct argument_reader + { + wl_argument* args{ nullptr }; + std::size_t current{ 0 }; + + wl_argument next_arg() + { + assert(args != nullptr && "expected argument reader to still be alive"); + return args[current++]; + } + + ref read_int() + { + return ref::steal(lean_box_uint32(next_arg().i)); + } + + ref read_uint() + { + return ref::steal(lean_box_uint32(next_arg().u)); + } + + ref read_fixed() + { + return ref::steal(lean_box_float(wl_fixed_to_double(next_arg().f))); + } + + ref read_string() + { + auto s = next_arg().s; + if (s) + { + auto res = ref::steal(lean_alloc_ctor(1, 1, 0)); + lean_ctor_set(res.get(), 0, lean_mk_string_from_bytes(s, strlen(s))); + return res; + } + else + { + return ref::steal(lean_box(0)); + } + } + + ref read_object() + { + auto o = next_arg().o; + if (o) + { + auto res = ref::steal(lean_alloc_ctor(1, 1, 0)); + auto proxy_obj = (lean_object*)(wl_proxy_get_listener((wl_proxy*)o)); // set as dispatcher_data + lean_inc(proxy_obj); + lean_ctor_set(res.get(), 0, proxy_obj); + return res; + } + else + { + return ref::steal(lean_box(0)); + } + } + + ref read_new_id() + { + return ref::steal(lean_box_uint32(next_arg().n)); + } + + ref read_array() + { + auto a = next_arg().a; + auto res = ref::steal(lean_alloc_sarray(1, a->size, a->size)); + std::copy_n(static_cast<uint8_t*>(a->data), a->size, lean_sarray_cptr(res.get())); + return res; + } + + ref read_fd() + { + return ref::steal(lean_box_uint32(next_arg().h)); + } + }; + + lean_external_class* waylean_argument_reader_class() + { + static lean_external_class* klass = lean_register_external_class( + [](void* ptr) { delete static_cast<argument_reader*>(ptr); }, + [](void*, b_lean_obj_arg fn) { } + ); + return klass; + } +} + +// ArgumentReader.readInt : (reader : @& ArgumentReader) → IO Int32 +lean_obj_res waylean_argument_reader_read_int(b_lean_obj_arg reader_obj) +{ + auto reader = static_cast<argument_reader*>(lean_get_external_data(reader_obj)); + return lean_io_result_mk_ok(reader->read_int().release()); +} + +// ArgumentReader.readUInt : (reader : @& ArgumentReader) → IO Int32 +lean_obj_res waylean_argument_reader_read_uint(b_lean_obj_arg reader_obj) +{ + auto reader = static_cast<argument_reader*>(lean_get_external_data(reader_obj)); + return lean_io_result_mk_ok(reader->read_uint().release()); +} + +// ArgumentReader.readFixed : (reader : @& ArgumentReader) → IO Float +lean_obj_res waylean_argument_reader_read_fixed(b_lean_obj_arg reader_obj) +{ + auto reader = static_cast<argument_reader*>(lean_get_external_data(reader_obj)); + return lean_io_result_mk_ok(reader->read_fixed().release()); +} + +// ArgumentReader.readString : (reader : @& ArgumentReader) → IO (Option String) +lean_obj_res waylean_argument_reader_read_string(b_lean_obj_arg reader_obj) +{ + auto reader = static_cast<argument_reader*>(lean_get_external_data(reader_obj)); + return lean_io_result_mk_ok(reader->read_string().release()); +} + +// ArgumentReader.readObject : (reader : @& ArgumentReader) → IO (Option Proxy) +lean_obj_res waylean_argument_reader_read_object(b_lean_obj_arg reader_obj) +{ + auto reader = static_cast<argument_reader*>(lean_get_external_data(reader_obj)); + return lean_io_result_mk_ok(reader->read_object().release()); +} + +// ArgumentReader.readNewID : (reader : @& ArgumentReader) → IO UInt32 +lean_obj_res waylean_argument_reader_read_new_id(b_lean_obj_arg reader_obj) +{ + auto reader = static_cast<argument_reader*>(lean_get_external_data(reader_obj)); + return lean_io_result_mk_ok(reader->read_new_id().release()); +} + +// ArgumentReader.readArray : (reader : @& ArgumentReader) → IO ByteArray +lean_obj_res waylean_argument_reader_read_array(b_lean_obj_arg reader_obj) +{ + auto reader = static_cast<argument_reader*>(lean_get_external_data(reader_obj)); + return lean_io_result_mk_ok(reader->read_array().release()); +} + +// ArgumentReader.readFD : (reader : @& ArgumentReader) → IO Int32 +lean_obj_res waylean_argument_reader_read_fd(b_lean_obj_arg reader_obj) +{ + auto reader = static_cast<argument_reader*>(lean_get_external_data(reader_obj)); + return lean_io_result_mk_ok(reader->read_fd().release()); +} + // -- Proxy -// Proxy.fromDisplay : (display : @& Display) → IO Proxy -lean_obj_res waylean_proxy_from_display(b_lean_obj_arg display) +namespace +{ + int dispatcher_func(const void* user_data, void* target, uint32_t opcode, const wl_message* msg, wl_argument* args) + { + if (!user_data) { return 0; } + + auto handler = ref{ (lean_object*)user_data }; + auto reader = new argument_reader; + auto reader_obj = ref::steal(lean_alloc_external(waylean_argument_reader_class(), reader)); + + reader->args = args; + auto tuple = ref::steal( + lean_apply_2( + std::move(handler).release(), + lean_box_uint32(opcode), + std::move(reader_obj).release() + ) + ); + // TODO: Won't work because reader is only used in the event loop. + reader->args = nullptr; + + auto loop_obj = lean_ctor_get(tuple.get(), 0); + auto loop = static_cast<event_loop*>(lean_get_external_data(loop_obj)); + auto message_obj = lean_ctor_get(tuple.get(), 1); + + loop->queue_display_message(ref{ message_obj }); + + return 0; + } + + lean_external_class* waylean_proxy_class() + { + static lean_external_class* klass = lean_register_external_class( + [](void* ptr) + { + auto proxy = static_cast<wl_proxy*>(ptr); + if (auto user_data = wl_proxy_get_user_data(proxy)) + { + lean_dec(static_cast<lean_object*>(user_data)); + } + wl_proxy_destroy(proxy); + }, + [](void*, b_lean_obj_arg fn) { } + ); + return klass; + } +} + +// Proxy.fromDisplay : (display : Display) → IO Proxy +lean_obj_res waylean_proxy_from_display(lean_obj_arg display) { + return lean_io_result_mk_ok(display); } // Proxy.new : (factory : @& Proxy) → (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Proxy -lean_obj_res waylean_proxy_new(b_lean_obj_arg factory, b_lean_obj_arg type_map, b_lean_obj_arg iface_name) +lean_obj_res waylean_proxy_new(b_lean_obj_arg factory_obj, b_lean_obj_arg map_obj, b_lean_obj_arg iface_name) { + auto factory = static_cast<wl_proxy*>(lean_get_external_data(factory_obj)); + auto map = static_cast<type_map*>(lean_get_external_data(map_obj)); + auto iface = map->resolve_iface(lean_string_cstr(iface_name)); + + assert(iface->initialized && "expected interface to be initialized during construction"); + wl_proxy* res = wl_proxy_create(factory, &iface->desc); + lean_object* waylean_res = lean_alloc_external(waylean_proxy_class(), res); + if (!res) { return io_result_mk_from_errno("<unknown>"); } + + wl_proxy_add_dispatcher(res, dispatcher_func, waylean_res, nullptr); + + return lean_io_result_mk_ok(waylean_res); } // Proxy.send : (proxy : @& Proxy) → (opcode : UInt32) → (argumentWriter : @& ArgumentWriter) → IO Unit -lean_obj_res waylean_proxy_send(b_lean_obj_arg proxy, uint32_t opcode, b_lean_obj_arg argument_writer) +lean_obj_res waylean_proxy_send(b_lean_obj_arg proxy_obj, uint32_t opcode, b_lean_obj_arg writer_obj) { + auto proxy = static_cast<wl_proxy*>(lean_get_external_data(proxy_obj)); + auto writer = static_cast<argument_writer*>(lean_get_external_data(writer_obj)); + wl_proxy_marshal_array(proxy, opcode, writer->get_args()); + return lean_io_result_mk_ok(lean_box(0)); } -// Proxy.listen : (proxy : @& Proxy) → (handler : @& UInt32 → ArgumentReader → EventLoop M × M) → IO Unit -lean_obj_res waylean_proxy_listen(b_lean_obj_arg proxy, b_lean_obj_arg handler) +// Proxy.listen : (proxy : @& Proxy) → (handler : UInt32 → ArgumentReader → EventLoop M × M) → IO Unit +lean_obj_res waylean_proxy_listen(b_lean_obj_arg proxy_obj, lean_obj_arg handler) { + auto proxy = static_cast<wl_proxy*>(lean_get_external_data(proxy_obj)); + auto old_data = static_cast<lean_object*>(wl_proxy_get_user_data(proxy)); + if (old_data) { lean_dec(old_data); } + wl_proxy_set_user_data(proxy, handler); + return lean_io_result_mk_ok(lean_box(0)); }
\ No newline at end of file diff --git a/lib/CWayland/CWayland.h b/lib/CWayland/CWayland.h index e0bcfa2..852cc7c 100644 --- a/lib/CWayland/CWayland.h +++ b/lib/CWayland/CWayland.h @@ -41,18 +41,6 @@ lean_obj_res waylean_type_map_contains(b_lean_obj_arg type_map, lean_obj_res waylean_type_map_register(b_lean_obj_arg type_map, b_lean_obj_arg iface_desc); -// -- Proxy - -lean_obj_res waylean_proxy_from_display(b_lean_obj_arg display); -lean_obj_res waylean_proxy_new (b_lean_obj_arg factory, - b_lean_obj_arg type_map, - b_lean_obj_arg iface_name); -lean_obj_res waylean_proxy_send (b_lean_obj_arg proxy, - uint32_t opcode, - b_lean_obj_arg argument_writer); -lean_obj_res waylean_proxy_listen (b_lean_obj_arg proxy, - b_lean_obj_arg handler); - // -- Argument Writer lean_obj_res waylean_argument_writer_new (void); @@ -84,6 +72,18 @@ lean_obj_res waylean_argument_reader_read_new_id(b_lean_obj_arg reader); lean_obj_res waylean_argument_reader_read_array (b_lean_obj_arg reader); lean_obj_res waylean_argument_reader_read_fd (b_lean_obj_arg reader); +// -- Proxy + +lean_obj_res waylean_proxy_from_display(lean_obj_arg display); +lean_obj_res waylean_proxy_new (b_lean_obj_arg factory, + b_lean_obj_arg type_map, + b_lean_obj_arg iface_name); +lean_obj_res waylean_proxy_send (b_lean_obj_arg proxy, + uint32_t opcode, + b_lean_obj_arg argument_writer); +lean_obj_res waylean_proxy_listen (b_lean_obj_arg proxy, + lean_obj_arg handler); + #ifdef __cplusplus } #endif
\ No newline at end of file diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean index d42147c..2e2ceaa 100644 --- a/lib/Wayland/Display.lean +++ b/lib/Wayland/Display.lean @@ -28,7 +28,8 @@ def OpCode : Type := UInt32 deriving Repr, Nonempty, BEq, OfNat /-- Handle to a client object, possibly dead. -/ -def Object (ι : InterfaceName) : Type := Native.Proxy +structure Object (ι : InterfaceName) : Type where + private proxy : Native.Proxy deriving Nonempty /-- Monad in which arguments can be marshalled one after another. -/ @@ -261,6 +262,19 @@ private def DisplayM.ensureInterface (ι : InterfaceName) [iface : ResolvedInter requests := iface'.requestClass.messages.map MessageDesc.toNative events := iface'.eventClass.messages.map MessageDesc.toNative } +/-- Get the `wl_display` instance within the display monad. -/ +def DisplayM.getDisplay : DisplayM σ (Object "wl_display") := do + let proxy ← Native.Proxy.fromDisplay (← read).disp + return ⟨proxy⟩ + +/-- Create a new object, allocating a new ID in the client space and inheriting the display from the `factory` +object. -/ +def DisplayM.createObject {ι ι' : InterfaceName} [iface : ResolvedInterface ι] (factory : Object ι') : DisplayM σ (Object ι) := do + ensureInterface ι + let typeMap := (← read).typeMap + let proxy ← Native.Proxy.new factory.proxy typeMap ι + return ⟨proxy⟩ + -- def Object.send [iface : Interface ι] (obj : Object ι) (req : iface.request) : DisplayM σ Unit := sorry -- def Object.listen [iface : Interface ι] (obj : Object ι) (handler : iface.event → DisplayM σ Unit) : DisplayM σ Unit := sorry diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean index f889c25..909cde4 100644 --- a/lib/Wayland/Native.lean +++ b/lib/Wayland/Native.lean @@ -17,25 +17,25 @@ private opaque DisplayP : NonemptyType private opaque EventLoopP (M : Type) : NonemptyType private opaque EventSourceP : NonemptyType private opaque TypeMapP : NonemptyType -private opaque ProxyP : NonemptyType private opaque ArgumentReaderP : NonemptyType private opaque ArgumentWriterP : NonemptyType +private opaque ProxyP : NonemptyType def Display : Type := DisplayP.type def EventLoop (M : Type) : Type := (EventLoopP M).type def EventSource : Type := EventSourceP.type def TypeMap : Type := TypeMapP.type -def Proxy : Type := ProxyP.type def ArgumentReader : Type := ArgumentReaderP.type def ArgumentWriter : Type := ArgumentWriterP.type +def Proxy : Type := ProxyP.type instance : Nonempty Display := DisplayP.property instance : Nonempty (EventLoop M) := (EventLoopP M).property instance : Nonempty EventSource := EventSourceP.property instance : Nonempty TypeMap := TypeMapP.property -instance : Nonempty Proxy := ProxyP.property instance : Nonempty ArgumentReader := ArgumentReaderP.property instance : Nonempty ArgumentWriter := ArgumentWriterP.property +instance : Nonempty Proxy := ProxyP.property @[extern "waylean_SIGINT"] opaque SIGINT (u : Unit) : UInt32 @@ -49,9 +49,6 @@ opaque SIGUSR2 (u : Unit) : UInt32 @[extern "waylean_display_new"] opaque Display.new : (name : @& Option String) → IO Display -@[extern "waylean_display_roundtrip"] -opaque Display.roundtrip : (display : @& Display) → IO Unit - @[extern "waylean_event_loop_new"] opaque EventLoop.new : IO (EventLoop M) @@ -82,8 +79,59 @@ opaque TypeMap.contains : (typeMap : @& TypeMap) → (ifaceName : @& String) → @[extern "waylean_type_map_register"] opaque TypeMap.register : (typeMap : @& TypeMap) → (ifaceDesc : @& Interface) → IO Unit +@[extern "waylean_argument_writer_new"] +opaque ArgumentWriter.new : IO ArgumentWriter + +@[extern "waylean_argument_writer_write_int"] +opaque ArgumentWriter.writeInt : (writer : @& ArgumentWriter) → (value : Int32) → IO Unit + +@[extern "waylean_argument_writer_write_uint"] +opaque ArgumentWriter.writeUInt : (writer : @& ArgumentWriter) → (value : UInt32) → IO Unit + +@[extern "waylean_argument_writer_write_fixed"] +opaque ArgumentWriter.writeFloat : (writer : @& ArgumentWriter) → (value : Float) → IO Unit + +@[extern "waylean_argument_writer_write_string"] +opaque ArgumentWriter.writeString : (writer : @& ArgumentWriter) → (value : @& Option String) → IO Unit + +@[extern "waylean_argument_writer_write_object"] +opaque ArgumentWriter.writeObject : (writer : @& ArgumentWriter) → (value : @& Option Proxy) → IO Unit + +@[extern "waylean_argument_writer_write_new_id"] +opaque ArgumentWriter.writeNewID : (writer : @& ArgumentWriter) → (value : @& Proxy) → IO Unit + +@[extern "waylean_argument_writer_write_array"] +opaque ArgumentWriter.writeArray : (writer : @& ArgumentWriter) → (value : @& ByteArray) → IO Unit + +@[extern "waylean_argument_writer_write_fd"] +opaque ArgumentWriter.writeFD : (writer : @& ArgumentWriter) → (value : Int32) → IO Unit + +@[extern "waylean_argument_reader_read_int"] +opaque ArgumentReader.readInt : (reader : @& ArgumentReader) → IO Int32 + +@[extern "waylean_argument_reader_read_uint"] +opaque ArgumentReader.readUInt : (reader : @& ArgumentReader) → IO Int32 + +@[extern "waylean_argument_reader_read_fixed"] +opaque ArgumentReader.readFixed : (reader : @& ArgumentReader) → IO Float + +@[extern "waylean_argument_reader_read_string"] +opaque ArgumentReader.readString : (reader : @& ArgumentReader) → IO (Option String) + +@[extern "waylean_argument_reader_read_object"] +opaque ArgumentReader.readObject : (reader : @& ArgumentReader) → IO (Option Proxy) + +@[extern "waylean_argument_reader_read_new_id"] +opaque ArgumentReader.readNewID : (reader : @& ArgumentReader) → IO UInt32 + +@[extern "waylean_argument_reader_read_array"] +opaque ArgumentReader.readArray : (reader : @& ArgumentReader) → IO ByteArray + +@[extern "waylean_argument_reader_read_fd"] +opaque ArgumentReader.readFD : (reader : @& ArgumentReader) → IO Int32 + @[extern "waylean_proxy_from_display"] -opaque Proxy.fromDisplay : (display : @& Display) → IO Proxy +opaque Proxy.fromDisplay : (display : Display) → IO Proxy @[extern "waylean_proxy_new"] opaque Proxy.new : (factory : @& Proxy) → (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Proxy @@ -92,6 +140,6 @@ opaque Proxy.new : (factory : @& Proxy) → (typeMap : @& TypeMap) → (ifaceNam opaque Proxy.send : (proxy : @& Proxy) → (opcode : UInt32) → (argumentWriter : @& ArgumentWriter) → IO Unit @[extern "waylean_proxy_listen"] -opaque Proxy.listen : (proxy : @& Proxy) → (handler : @& (UInt32 → ArgumentReader → EventLoop M × M)) → IO Unit +opaque Proxy.listen : (proxy : @& Proxy) → (handler : UInt32 → ArgumentReader → EventLoop M × M) → IO Unit end Wayland.Native |