first working version

13 files changed, 396 insertions, 288 deletions

diff --git a/lib/CWayland/CWayland.cc b/lib/CWayland/CWayland.cc
index 08df50b..88586bb 100644
--- a/lib/CWayland/CWayland.cc
+++ b/lib/CWayland/CWayland.cc
@@ -15,6 +15,7 @@
 #include <unistd.h>
 #include <stdio.h>
 #include <signal.h>
+#include <atomic>
 
 namespace
 {
@@ -104,6 +105,32 @@ namespace
         }
     };
 
+    struct stable_ptr
+    {
+        static inline std::atomic<std::uint64_t> current_id = 0;
+
+        std::uint64_t id;
+        void* ptr;
+        void (*destructor)(void*);
+
+        explicit stable_ptr(void* ptr, void (*destructor)(void*))
+            : id{ current_id++ }
+            , ptr{ ptr }
+            , destructor{ destructor }
+        {
+        }
+
+        stable_ptr(stable_ptr const&) = delete;
+        stable_ptr(stable_ptr&&) = delete;
+        stable_ptr& operator=(stable_ptr const&) = delete;
+        stable_ptr& operator=(stable_ptr&&) = delete;
+
+        ~stable_ptr()
+        {
+            if (ptr) { destructor(ptr); }
+        }
+    };
+
     char const* option_cstr_or_null(b_lean_obj_arg str)
     {
         if (lean_is_scalar(str))
@@ -126,6 +153,13 @@ namespace
         return lean_io_result_mk_error(error);
     }
 
+    lean_obj_res io_result_mk_resource_vanished()
+    {
+        ref file_name_str = ref::steal(lean_mk_string("<unknown>"));
+        lean_object* error = lean_decode_io_error(EIDRM, file_name_str.get());
+        return lean_io_result_mk_error(error);
+    }
+
     // Global dispatcher func, assumes a user_data of type (UInt32 → ArgumentBuffer → EventLoop M × M)
     int dispatcher_func(const void* user_data, void* target, uint32_t opcode, const wl_message* msg, wl_argument* args);
 }
@@ -154,19 +188,27 @@ namespace
     lean_external_class* waylean_display_class()
     {
         static lean_external_class* klass = lean_register_external_class(
-            [](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* ptr) { delete static_cast<stable_ptr*>(ptr); },
             [](void*, b_lean_obj_arg fn) { }
         );
         return klass;
     }
+
+    void waylean_proxy_deref_user_data(wl_proxy* proxy)
+    {
+        if (auto user_data = wl_proxy_get_user_data(proxy))
+        {
+            lean_dec(static_cast<lean_object*>(user_data));
+        }
+    }
+
+    void waylean_display_destructor(void* ptr)
+    {
+        auto proxy = static_cast<wl_proxy*>(ptr);
+        auto disp = static_cast<wl_display*>(ptr);
+        waylean_proxy_deref_user_data(proxy);
+        wl_display_disconnect(disp);
+    }
 }
 
 // Display.new : (name : @& Option String) → IO Display
@@ -175,7 +217,8 @@ 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);
+    auto sptr = new stable_ptr{ disp, waylean_display_destructor };
+    lean_object* waylean_disp = lean_alloc_external(waylean_display_class(), sptr);
 
     return lean_io_result_mk_ok(waylean_disp);
 }
@@ -183,7 +226,9 @@ lean_obj_res waylean_display_new(b_lean_obj_arg name)
 // Display.flush : (display : @& Display) → IO Unit
 lean_obj_res waylean_display_flush(b_lean_obj_arg disp_obj)
 {
-    wl_display* disp = static_cast<wl_display*>(lean_get_external_data(disp_obj));
+    auto sptr = static_cast<stable_ptr*>(lean_get_external_data(disp_obj));
+    auto disp = static_cast<wl_display*>(sptr->ptr);
+    if (!disp) { return io_result_mk_resource_vanished(); }
     if (wl_display_flush(disp) == -1) { return io_result_mk_from_errno("<unknown>"); }
     return lean_io_result_mk_ok(lean_box(0));
 }
@@ -281,7 +326,7 @@ namespace
     struct display_source
     {
         ref display_ref{};
-        wl_display* disp{};
+        stable_ptr* disp{};
         size_t id{};
     };
 
@@ -349,10 +394,13 @@ namespace
 
             for (auto& src : displays)
             {
-                pollfd disp_pollfd{};
-                disp_pollfd.fd = wl_display_get_fd(src.disp);
-                disp_pollfd.events = POLLIN;
-                pollfds.emplace_back(disp_pollfd);
+                if (auto disp = static_cast<wl_display*>(src.disp->ptr))
+                {
+                    pollfd disp_pollfd{};
+                    disp_pollfd.fd = wl_display_get_fd(disp);
+                    disp_pollfd.events = POLLIN;
+                    pollfds.emplace_back(disp_pollfd);
+                }
             }
         }
 
@@ -378,7 +426,7 @@ namespace
             res.id = next_id++;
 
             auto source = display_source{};
-            source.disp = static_cast<wl_display*>(lean_get_external_data(display.get()));
+            source.disp = static_cast<stable_ptr*>(lean_get_external_data(display.get()));
             source.display_ref = std::move(display);
             source.id = res.id;
             displays.emplace_back(std::move(source));
@@ -482,14 +530,17 @@ namespace
                 for (auto& src : displays)
                 {
                     dispatching_display = src.id;
-                    while (wl_display_prepare_read(src.disp))
+                    if (auto disp = static_cast<wl_display*>(src.disp->ptr))
                     {
-                        return ref::steal(io_result_mk_from_errno("<default>"));
-                    }
+                        while (wl_display_prepare_read(disp))
+                        {
+                            return ref::steal(io_result_mk_from_errno("<default>"));
+                        }
 
-                    if (wl_display_flush(src.disp) == -1)
-                    {
-                        return ref::steal(io_result_mk_from_errno("<default>"));
+                        if (wl_display_flush(disp) == -1)
+                        {
+                            return ref::steal(io_result_mk_from_errno("<default>"));
+                        }
                     }
                 }
                 
@@ -533,13 +584,16 @@ namespace
                 for (auto& src : displays)
                 {
                     dispatching_display = src.id;
-                    if (wl_display_read_events(src.disp) == -1)
-                    {
-                        return ref::steal(io_result_mk_from_errno("<default>"));
-                    }
-                    if (wl_display_dispatch_pending(src.disp) == -1)
+                    if (auto disp = static_cast<wl_display*>(src.disp->ptr))
                     {
-                        return ref::steal(io_result_mk_from_errno("<default>"));
+                        if (wl_display_read_events(disp) == -1)
+                        {
+                            return ref::steal(io_result_mk_from_errno("<default>"));
+                        }
+                        if (wl_display_dispatch_pending(disp) == -1)
+                        {
+                            return ref::steal(io_result_mk_from_errno("<default>"));
+                        }
                     }
                 }
 
@@ -905,17 +959,10 @@ namespace
             meta[i].r = std::move(value);
         }
 
-        void write_object(ref value)
+        void write_object(ref value, wl_object* value_obj)
         {
             auto i = next_write();
-            if (lean_is_scalar(value.get()))
-            {
-                args[i].o = nullptr;
-            }
-            else
-            {
-                args[i].o = static_cast<wl_object*>(lean_get_external_data(lean_ctor_get(value.get(), 0)));
-            }
+            args[i].o = value_obj;
             meta[i].t = type::object;
             meta[i].r = std::move(value);
         }
@@ -1101,7 +1148,14 @@ lean_obj_res waylean_argument_buffer_write_string(b_lean_obj_arg buffer_obj, b_l
 lean_obj_res waylean_argument_buffer_write_object(b_lean_obj_arg buffer_obj, b_lean_obj_arg value)
 {
     auto buffer = static_cast<argument_buffer*>(lean_get_external_data(buffer_obj));
-    buffer->write_object(ref{ value });
+    wl_object* obj = nullptr;
+    if (!lean_is_scalar(value))
+    {
+        auto sptr = static_cast<stable_ptr*>(lean_get_external_data(lean_ctor_get(value, 0)));
+        obj = static_cast<wl_object*>(sptr->ptr);
+        if (!obj) { return io_result_mk_resource_vanished(); }
+    }
+    buffer->write_object(ref{ value }, obj);
     return lean_io_result_mk_ok(lean_box(0));
 }
 
@@ -1219,23 +1273,23 @@ namespace
     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* ptr) { delete static_cast<stable_ptr*>(ptr); },
             [](void*, b_lean_obj_arg fn) { }
         );
         return klass;
     }
 
+    void waylean_proxy_destructor(void* ptr)
+    {
+        auto proxy = static_cast<wl_proxy*>(ptr);
+        waylean_proxy_deref_user_data(proxy);
+        wl_proxy_destroy(proxy);
+    }
+
     ref init_proxy_wrapper(wl_proxy* proxy)
     {
-        lean_object* waylean_res = lean_alloc_external(waylean_proxy_class(), proxy);
+        auto sptr = new stable_ptr{ proxy, waylean_proxy_destructor };
+        auto waylean_res = lean_alloc_external(waylean_proxy_class(), sptr);
         wl_proxy_add_dispatcher(proxy, dispatcher_func, waylean_res, nullptr);
 
         return ref::steal(waylean_res);
@@ -1248,27 +1302,55 @@ lean_obj_res waylean_proxy_from_display(lean_obj_arg display)
     return lean_io_result_mk_ok(display);
 }
 
-// Proxy.send : (proxy : @& Proxy) → (opcode : UInt32) → (argumentBuffer : @& ArgumentBuffer) → IO Unit
-lean_obj_res waylean_proxy_send(b_lean_obj_arg proxy_obj, uint32_t opcode, b_lean_obj_arg buffer_obj)
+// Proxy.send : (proxy : @& Proxy) → (opcode : UInt32) → (argumentBuffer : @& ArgumentBuffer) → (destroy : UInt32) → IO Unit
+lean_obj_res waylean_proxy_send(b_lean_obj_arg proxy_obj, uint32_t opcode, b_lean_obj_arg buffer_obj, uint32_t destroy)
 {
-    auto proxy = static_cast<wl_proxy*>(lean_get_external_data(proxy_obj));
+    auto sptr = static_cast<stable_ptr*>(lean_get_external_data(proxy_obj));
+    auto proxy = static_cast<wl_proxy*>(sptr->ptr);
+    if (!proxy) { return io_result_mk_resource_vanished(); }
+
     auto buffer = static_cast<argument_buffer*>(lean_get_external_data(buffer_obj));
 
-    wl_proxy_marshal_array(proxy, opcode, buffer->get_args());
+    wl_proxy_marshal_array_flags(
+        proxy,
+        opcode,
+        nullptr,
+        wl_proxy_get_version(proxy),
+        destroy ? WL_MARSHAL_FLAG_DESTROY : 0,
+        buffer->get_args());
+    if (destroy)
+    {
+        waylean_proxy_deref_user_data(proxy);
+        sptr->ptr = nullptr;
+    }
     
     return lean_io_result_mk_ok(lean_box(0));
 }
 
-// Proxy.sendConstructor : (proxy : @& Proxy) → (opcode : UInt32) → (argumentBuffer : @& ArgumentBuffer) → (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Proxy
-lean_obj_res waylean_proxy_send_constructor(b_lean_obj_arg proxy_obj, uint32_t opcode, b_lean_obj_arg buffer_obj, b_lean_obj_arg map_obj, b_lean_obj_arg iface_name)
+// Proxy.sendConstructor : (proxy : @& Proxy) → (opcode : UInt32) → (argumentBuffer : @& ArgumentBuffer) → (destroy : UInt32) → (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Proxy
+lean_obj_res waylean_proxy_send_constructor(b_lean_obj_arg proxy_obj, uint32_t opcode, b_lean_obj_arg buffer_obj, uint32_t destroy, b_lean_obj_arg map_obj, b_lean_obj_arg iface_name)
 {
-    auto proxy = static_cast<wl_proxy*>(lean_get_external_data(proxy_obj));
+    auto sptr = static_cast<stable_ptr*>(lean_get_external_data(proxy_obj));
+    auto proxy = static_cast<wl_proxy*>(sptr->ptr);
+    if (!proxy) { return io_result_mk_resource_vanished(); }
+
     auto buffer = static_cast<argument_buffer*>(lean_get_external_data(buffer_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->is_complete && "expected interface to be initialized during construction");
 
-    wl_proxy* res = wl_proxy_marshal_array_constructor(proxy, opcode, buffer->get_args(), &iface->desc);
+    wl_proxy* res = wl_proxy_marshal_array_flags(
+        proxy,
+        opcode,
+        &iface->desc,
+        wl_proxy_get_version(proxy),
+        destroy ? WL_MARSHAL_FLAG_DESTROY : 0,
+        buffer->get_args());
+    if (destroy)
+    {
+        waylean_proxy_deref_user_data(proxy);
+        sptr->ptr = nullptr;
+    }
     if (!res) { return io_result_mk_from_errno("<unknown>"); }
 
     return lean_io_result_mk_ok(init_proxy_wrapper(res).release());
@@ -1277,7 +1359,10 @@ lean_obj_res waylean_proxy_send_constructor(b_lean_obj_arg proxy_obj, uint32_t o
 // Proxy.listen : (proxy : @& Proxy) → (handler : UInt32 → ArgumentBuffer → 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 sptr = static_cast<stable_ptr*>(lean_get_external_data(proxy_obj));
+    auto proxy = static_cast<wl_proxy*>(sptr->ptr);
+    if (!proxy) { return io_result_mk_resource_vanished(); }
+
     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);
@@ -1294,14 +1379,27 @@ lean_obj_res waylean_proxy_keep(b_lean_obj_arg proxy)
 // Proxy.getType : (proxy : @& Proxy) → IO String
 lean_obj_res waylean_proxy_get_type(b_lean_obj_arg proxy_obj)
 {
-    auto proxy = static_cast<wl_proxy*>(lean_get_external_data(proxy_obj));
+    auto sptr = static_cast<stable_ptr*>(lean_get_external_data(proxy_obj));
+    auto proxy = static_cast<wl_proxy*>(sptr->ptr);
+    if (!proxy) { return io_result_mk_resource_vanished(); }
+
     auto name = wl_proxy_get_interface(proxy)->name;
     return lean_io_result_mk_ok(lean_mk_string(name));
 }
 
 // Proxy.getID : (x : @& Proxy) → IO UInt64
-lean_obj_res waylean_proxy_get_id(b_lean_obj_arg x)
+lean_obj_res waylean_proxy_get_id(b_lean_obj_arg proxy_obj)
 {
-    auto proxy = static_cast<wl_proxy*>(lean_get_external_data(x));
+    auto sptr = static_cast<stable_ptr*>(lean_get_external_data(proxy_obj));
+    auto proxy = static_cast<wl_proxy*>(sptr->ptr);
+    if (!proxy) { return io_result_mk_resource_vanished(); }
+
     return lean_io_result_mk_ok(lean_box_uint64(wl_proxy_get_id(proxy)));
+}
+
+// Proxy.getStableID : (x : @& Proxy) → IO UInt64
+lean_obj_res waylean_proxy_get_stable_id(b_lean_obj_arg proxy_obj)
+{
+    auto sptr = static_cast<stable_ptr*>(lean_get_external_data(proxy_obj));
+    return lean_io_result_mk_ok(lean_box_uint64(sptr->id));
 }
\ No newline at end of file
diff --git a/lib/CWayland/CWayland.h b/lib/CWayland/CWayland.h
index ff71348..1805b9f 100644
--- a/lib/CWayland/CWayland.h
+++ b/lib/CWayland/CWayland.h
@@ -73,10 +73,12 @@ lean_obj_res waylean_argument_buffer_read_fd     (b_lean_obj_arg reader);
 lean_obj_res waylean_proxy_from_display    (lean_obj_arg   display);
 lean_obj_res waylean_proxy_send            (b_lean_obj_arg proxy,
                                             uint32_t       opcode,
-                                            b_lean_obj_arg argument_buffer);
+                                            b_lean_obj_arg argument_buffer,
+                                            uint32_t       destroy);
 lean_obj_res waylean_proxy_send_constructor(b_lean_obj_arg proxy,
                                             uint32_t       opcode,
                                             b_lean_obj_arg argument_buffer,
+                                            uint32_t       destroy,
                                             b_lean_obj_arg type_map,
                                             b_lean_obj_arg iface_name);
 lean_obj_res waylean_proxy_listen          (b_lean_obj_arg proxy,
@@ -84,6 +86,7 @@ lean_obj_res waylean_proxy_listen          (b_lean_obj_arg proxy,
 lean_obj_res waylean_proxy_keep            (b_lean_obj_arg proxy);
 lean_obj_res waylean_proxy_get_type        (b_lean_obj_arg proxy);
 lean_obj_res waylean_proxy_get_id          (b_lean_obj_arg x);
+lean_obj_res waylean_proxy_get_stable_id   (b_lean_obj_arg x);
 
 #ifdef __cplusplus
 }
diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean
index d82a951..728b313 100644
--- a/lib/Wayland/Display.lean
+++ b/lib/Wayland/Display.lean
@@ -34,14 +34,14 @@ def Fd : Type := Int32
 /-- Handle to a client object, possibly dead. -/
 structure Object (ι : InterfaceName) : Type where
   private proxy : Native.Proxy
-  private id : UInt64
+  private stableID : UInt64
   deriving Nonempty
 
 /-- Opaque handle to an object whose type is not statically known. -/
 structure AnyObject : Type where
   private proxy : Native.Proxy
   private type : String
-  private id : UInt64
+  private stableID : UInt64
   deriving Nonempty
 
 /-- Monad in which arguments can be marshalled one after another. -/
@@ -281,11 +281,11 @@ private instance : ArgumentDemarshaller (ExceptT String ArgumentBufferM) where
   demarshalObject := do
     let proxy ← (← read).readObject
     proxy.mapM fun proxy ↦ do
-      return ⟨proxy, ← proxy.getID⟩
+      return ⟨proxy, ← proxy.getStableID⟩
   demarshalAnyObject := do
     let proxy ← (← read).readObject
     proxy.mapM fun proxy ↦ do
-      return ⟨proxy, ← proxy.getType, ← proxy.getID⟩
+      return ⟨proxy, ← proxy.getType, ← proxy.getStableID⟩
   demarshalArray := do (← read).readArray
   demarshalFd := do (← read).readFd
 
@@ -415,21 +415,21 @@ private def DisplayM.ensureInterface (ι : InterfaceName) [iface : ResolvedInter
 
 def DisplayM.getDisplay' : DisplayM σ (Object "wl_display") := do
   let proxy ← Native.Proxy.fromDisplay (← read).disp
-  return ⟨proxy, ← proxy.getID⟩
+  return ⟨proxy, ← proxy.getStableID⟩
 
 variable {ι ι' : InterfaceName}
 
 instance : BEq (Object ι) where
-  beq x y := x.id == y.id
+  beq x y := x.stableID == y.stableID
 
 instance : Hashable (Object ι) where
-  hash x := x.id
+  hash x := x.stableID
 
 instance : BEq AnyObject where
-  beq x y := x.id == y.id
+  beq x y := x.stableID == y.stableID
 
 instance : Hashable AnyObject where
-  hash x := x.id
+  hash x := x.stableID
 
 private def marshalArguments (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : IO (Native.ArgumentBuffer × OpCode) := do
   let argBuffer ← Native.ArgumentBuffer.new
@@ -438,17 +438,17 @@ private def marshalArguments (marshaller : ∀ {α} [ArgumentMarshaller α], α
   return (argBuffer, opcode)
 
 /-- Send a request for an object to the server that doesn't construct any new object. -/
-def Object.send (obj : Object ι) (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : DisplayM σ Unit := do
+def Object.send (obj : Object ι) (destroy : Bool) (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : DisplayM σ Unit := do
   let (argBuffer, opcode) ← marshalArguments marshaller
-  obj.proxy.send opcode argBuffer
+  obj.proxy.send opcode argBuffer (if destroy then 1 else 0)
 
 /-- Send a request for an object to the server, allocating a new id for a constructed object in the process. -/
-def Object.sendConstructor [iface : ResolvedInterface ι'] (obj : Object ι) (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : DisplayM σ (Object ι') := do
+def Object.sendConstructor [iface : ResolvedInterface ι'] (obj : Object ι) (destroy : Bool) (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : DisplayM σ (Object ι') := do
   DisplayM.ensureInterface ι'
   let typeMap := (← read).typeMap
   let (argBuffer, opcode) ← marshalArguments marshaller
-  let proxy ← obj.proxy.sendConstructor opcode argBuffer typeMap ι'
-  return ⟨proxy, ← proxy.getID⟩
+  let proxy ← obj.proxy.sendConstructor opcode argBuffer (if destroy then 1 else 0) typeMap ι'
+  return ⟨proxy, ← proxy.getStableID⟩
 
 /-- Listen for events from the server for an object. -/
 def Object.listen [iface : Interface ι] (obj : Object ι) (handler : iface.event → DisplayM σ Unit) : DisplayM σ Unit := do
@@ -465,11 +465,19 @@ def Object.keep (obj : Object ι) : DisplayM σ Unit :=
 
 /-- Erase the type information from an object. -/
 def Object.toAny (obj : Object ι) : AnyObject :=
-  ⟨obj.proxy, ι, obj.id⟩
+  ⟨obj.proxy, ι, obj.stableID⟩
+
+/-- Get the Wayland Object ID. -/
+def Object.getID (obj : Object ι) : DisplayM σ UInt64 :=
+  obj.proxy.getID
 
 /-- Try to cast a type-erased object into a typed object. -/
 def AnyObject.cast (obj : AnyObject) : Option (Object ι) :=
-  if obj.type == ι then .some ⟨obj.proxy, obj.id⟩ else .none
+  if obj.type == ι then .some ⟨obj.proxy, obj.stableID⟩ else .none
+
+/-- Get the Wayland Object ID. -/
+def AnyObject.getID (obj : AnyObject) : DisplayM σ UInt64 :=
+  obj.proxy.getID
 
 end Proxies
 
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean
index 72b0cf2..9158e6d 100644
--- a/lib/Wayland/Native.lean
+++ b/lib/Wayland/Native.lean
@@ -128,10 +128,10 @@ opaque ArgumentBuffer.readFd : (reader : @& ArgumentBuffer) → IO Int32
 opaque Proxy.fromDisplay : (display : Display) → IO Proxy
 
 @[extern "waylean_proxy_send"]
-opaque Proxy.send : (proxy : @& Proxy) → (opcode : UInt32) → (argumentBuffer : @& ArgumentBuffer) → IO Unit
+opaque Proxy.send : (proxy : @& Proxy) → (opcode : UInt32) → (argumentBuffer : @& ArgumentBuffer) → (destroy : UInt32) → IO Unit
 
 @[extern "waylean_proxy_send_constructor"]
-opaque Proxy.sendConstructor : (proxy : @& Proxy) → (opcode : UInt32) → (argumentBuffer : @& ArgumentBuffer) → (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Proxy
+opaque Proxy.sendConstructor : (proxy : @& Proxy) → (opcode : UInt32) → (argumentBuffer : @& ArgumentBuffer) → (destroy : UInt32) → (typeMap : @& TypeMap) → (ifaceName : @& String) → IO Proxy
 
 @[extern "waylean_proxy_listen"]
 opaque Proxy.listen : (proxy : @& Proxy) → (handler : UInt32 → ArgumentBuffer → EventLoop M × M) → IO Unit
@@ -145,4 +145,7 @@ opaque Proxy.getType : (proxy : @& Proxy) → IO String
 @[extern "waylean_proxy_get_id"]
 opaque Proxy.getID : (x : @& Proxy) → IO UInt64
 
+@[extern "waylean_proxy_get_stable_id"]
+opaque Proxy.getStableID : (x : @& Proxy) → IO UInt64
+
 end Wayland.Native
diff --git a/lib/Wayland/Protocols/RiverInputManagementV1/Requests.lean b/lib/Wayland/Protocols/RiverInputManagementV1/Requests.lean
index 3c9c44e..d20182e 100644
--- a/lib/Wayland/Protocols/RiverInputManagementV1/Requests.lean
+++ b/lib/Wayland/Protocols/RiverInputManagementV1/Requests.lean
@@ -9,20 +9,20 @@ variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι]
 def RiverInputManagerV1.stop
     (ω : RiverInputManagerV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 0
 
 def RiverInputManagerV1.destroy
     (ω : RiverInputManagerV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 1
 
 def RiverInputManagerV1.createSeat
     (ω : RiverInputManagerV1)
     (name : String)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .string name
     return 2
 
@@ -30,21 +30,21 @@ def RiverInputManagerV1.destroySeat
     (ω : RiverInputManagerV1)
     (name : String)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .string name
     return 3
 
 def RiverInputDeviceV1.destroy
     (ω : RiverInputDeviceV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def RiverInputDeviceV1.assignToSeat
     (ω : RiverInputDeviceV1)
     (name : String)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .string name
     return 1
 
@@ -53,7 +53,7 @@ def RiverInputDeviceV1.setRepeatInfo
     (rate : Int32)
     (delay : Int32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .int rate
     Marshallable.marshal .int delay
     return 2
@@ -62,7 +62,7 @@ def RiverInputDeviceV1.setScrollFactor
     (ω : RiverInputDeviceV1)
     (factor : Float32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .fixed factor
     return 3
 
@@ -70,7 +70,7 @@ def RiverInputDeviceV1.mapToOutput
     (ω : RiverInputDeviceV1)
     (output : Option WlOutput)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .object output
     return 4
 
@@ -81,7 +81,7 @@ def RiverInputDeviceV1.mapToRectangle
     (width : Int32)
     (height : Int32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .int x
     Marshallable.marshal .int y
     Marshallable.marshal .int width
diff --git a/lib/Wayland/Protocols/RiverLayerShellV1/Requests.lean b/lib/Wayland/Protocols/RiverLayerShellV1/Requests.lean
index 8e7dc9f..6cbdaab 100644
--- a/lib/Wayland/Protocols/RiverLayerShellV1/Requests.lean
+++ b/lib/Wayland/Protocols/RiverLayerShellV1/Requests.lean
@@ -9,14 +9,14 @@ variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι]
 def RiverLayerShellV1.destroy
     (ω : RiverLayerShellV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def RiverLayerShellV1.getOutput
     (ω : RiverLayerShellV1)
     (output : RiverOutputV1)
     : DisplayM σ RiverLayerShellOutputV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .object output
     return 1
@@ -25,7 +25,7 @@ def RiverLayerShellV1.getSeat
     (ω : RiverLayerShellV1)
     (seat : RiverSeatV1)
     : DisplayM σ RiverLayerShellSeatV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .object seat
     return 2
@@ -33,19 +33,19 @@ def RiverLayerShellV1.getSeat
 def RiverLayerShellOutputV1.destroy
     (ω : RiverLayerShellOutputV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def RiverLayerShellOutputV1.setDefault
     (ω : RiverLayerShellOutputV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 1
 
 def RiverLayerShellSeatV1.destroy
     (ω : RiverLayerShellSeatV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 end Wayland.Protocols
\ No newline at end of file
diff --git a/lib/Wayland/Protocols/RiverLibinputConfigV1/Requests.lean b/lib/Wayland/Protocols/RiverLibinputConfigV1/Requests.lean
index 12fb676..3c8e486 100644
--- a/lib/Wayland/Protocols/RiverLibinputConfigV1/Requests.lean
+++ b/lib/Wayland/Protocols/RiverLibinputConfigV1/Requests.lean
@@ -9,20 +9,20 @@ variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι]
 def RiverLibinputConfigV1.stop
     (ω : RiverLibinputConfigV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 0
 
 def RiverLibinputConfigV1.destroy
     (ω : RiverLibinputConfigV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 1
 
 def RiverLibinputConfigV1.createAccelConfig
     (ω : RiverLibinputConfigV1)
     (profile : RiverLibinputDeviceV1.AccelProfile)
     : DisplayM σ RiverLibinputAccelConfigV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .uint profile
     return 2
@@ -30,14 +30,14 @@ def RiverLibinputConfigV1.createAccelConfig
 def RiverLibinputDeviceV1.destroy
     (ω : RiverLibinputDeviceV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def RiverLibinputDeviceV1.setSendEvents
     (ω : RiverLibinputDeviceV1)
     (mode : RiverLibinputDeviceV1.SendEventsModes)
     : DisplayM σ RiverLibinputResultV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .uint mode
     return 1
@@ -46,7 +46,7 @@ def RiverLibinputDeviceV1.setTap
     (ω : RiverLibinputDeviceV1)
     (state : RiverLibinputDeviceV1.TapState)
     : DisplayM σ RiverLibinputResultV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .uint state
     return 2
@@ -55,7 +55,7 @@ def RiverLibinputDeviceV1.setTapButtonMap
     (ω : RiverLibinputDeviceV1)
     (buttonMap : RiverLibinputDeviceV1.TapButtonMap)
     : DisplayM σ RiverLibinputResultV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .uint buttonMap
     return 3
@@ -64,7 +64,7 @@ def RiverLibinputDeviceV1.setDrag
     (ω : RiverLibinputDeviceV1)
     (state : RiverLibinputDeviceV1.DragState)
     : DisplayM σ RiverLibinputResultV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .uint state
     return 4
@@ -73,7 +73,7 @@ def RiverLibinputDeviceV1.setDragLock
     (ω : RiverLibinputDeviceV1)
     (state : RiverLibinputDeviceV1.DragLockState)
     : DisplayM σ RiverLibinputResultV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .uint state
     return 5
@@ -82,7 +82,7 @@ def RiverLibinputDeviceV1.setThreeFingerDrag
     (ω : RiverLibinputDeviceV1)
     (state : RiverLibinputDeviceV1.ThreeFingerDragState)
     : DisplayM σ RiverLibinputResultV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .uint state
     return 6
@@ -91,7 +91,7 @@ def RiverLibinputDeviceV1.setCalibrationMatrix
     (ω : RiverLibinputDeviceV1)
     (matrix : ByteArray)
     : DisplayM σ RiverLibinputResultV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .array matrix
     return 7
@@ -100,7 +100,7 @@ def RiverLibinputDeviceV1.setAccelProfile
     (ω : RiverLibinputDeviceV1)
     (profile : RiverLibinputDeviceV1.AccelProfile)
     : DisplayM σ RiverLibinputResultV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .uint profile
     return 8
@@ -109,7 +109,7 @@ def RiverLibinputDeviceV1.setAccelSpeed
     (ω : RiverLibinputDeviceV1)
     (speed : ByteArray)
     : DisplayM σ RiverLibinputResultV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .array speed
     return 9
@@ -118,7 +118,7 @@ def RiverLibinputDeviceV1.applyAccelConfig
     (ω : RiverLibinputDeviceV1)
     (config : RiverLibinputAccelConfigV1)
     : DisplayM σ RiverLibinputResultV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .object config
     return 10
@@ -127,7 +127,7 @@ def RiverLibinputDeviceV1.setNaturalScroll
     (ω : RiverLibinputDeviceV1)
     (state : RiverLibinputDeviceV1.NaturalScrollState)
     : DisplayM σ RiverLibinputResultV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .uint state
     return 11
@@ -136,7 +136,7 @@ def RiverLibinputDeviceV1.setLeftHanded
     (ω : RiverLibinputDeviceV1)
     (state : RiverLibinputDeviceV1.LeftHandedState)
     : DisplayM σ RiverLibinputResultV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .uint state
     return 12
@@ -145,7 +145,7 @@ def RiverLibinputDeviceV1.setClickMethod
     (ω : RiverLibinputDeviceV1)
     (method : RiverLibinputDeviceV1.ClickMethod)
     : DisplayM σ RiverLibinputResultV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .uint method
     return 13
@@ -154,7 +154,7 @@ def RiverLibinputDeviceV1.setClickfingerButtonMap
     (ω : RiverLibinputDeviceV1)
     (buttonMap : RiverLibinputDeviceV1.ClickfingerButtonMap)
     : DisplayM σ RiverLibinputResultV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .uint buttonMap
     return 14
@@ -163,7 +163,7 @@ def RiverLibinputDeviceV1.setMiddleEmulation
     (ω : RiverLibinputDeviceV1)
     (state : RiverLibinputDeviceV1.MiddleEmulationState)
     : DisplayM σ RiverLibinputResultV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .uint state
     return 15
@@ -172,7 +172,7 @@ def RiverLibinputDeviceV1.setScrollMethod
     (ω : RiverLibinputDeviceV1)
     (method : RiverLibinputDeviceV1.ScrollMethod)
     : DisplayM σ RiverLibinputResultV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .uint method
     return 16
@@ -181,7 +181,7 @@ def RiverLibinputDeviceV1.setScrollButton
     (ω : RiverLibinputDeviceV1)
     (button : UInt32)
     : DisplayM σ RiverLibinputResultV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .uint button
     return 17
@@ -190,7 +190,7 @@ def RiverLibinputDeviceV1.setScrollButtonLock
     (ω : RiverLibinputDeviceV1)
     (state : RiverLibinputDeviceV1.ScrollButtonLockState)
     : DisplayM σ RiverLibinputResultV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .uint state
     return 18
@@ -199,7 +199,7 @@ def RiverLibinputDeviceV1.setDwt
     (ω : RiverLibinputDeviceV1)
     (state : RiverLibinputDeviceV1.DwtState)
     : DisplayM σ RiverLibinputResultV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .uint state
     return 19
@@ -208,7 +208,7 @@ def RiverLibinputDeviceV1.setDwtp
     (ω : RiverLibinputDeviceV1)
     (state : RiverLibinputDeviceV1.DwtpState)
     : DisplayM σ RiverLibinputResultV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .uint state
     return 20
@@ -217,7 +217,7 @@ def RiverLibinputDeviceV1.setRotation
     (ω : RiverLibinputDeviceV1)
     (angle : UInt32)
     : DisplayM σ RiverLibinputResultV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .uint angle
     return 21
@@ -225,7 +225,7 @@ def RiverLibinputDeviceV1.setRotation
 def RiverLibinputAccelConfigV1.destroy
     (ω : RiverLibinputAccelConfigV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def RiverLibinputAccelConfigV1.setPoints
@@ -234,7 +234,7 @@ def RiverLibinputAccelConfigV1.setPoints
     (step : ByteArray)
     (points : ByteArray)
     : DisplayM σ RiverLibinputResultV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .uint type
     Marshallable.marshal .array step
diff --git a/lib/Wayland/Protocols/RiverWindowManagementV1/Requests.lean b/lib/Wayland/Protocols/RiverWindowManagementV1/Requests.lean
index ed70fed..4a52ddc 100644
--- a/lib/Wayland/Protocols/RiverWindowManagementV1/Requests.lean
+++ b/lib/Wayland/Protocols/RiverWindowManagementV1/Requests.lean
@@ -10,38 +10,38 @@ variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι]
 def RiverWindowManagerV1.stop
     (ω : RiverWindowManagerV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 0
 
 def RiverWindowManagerV1.destroy
     (ω : RiverWindowManagerV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 1
 
 def RiverWindowManagerV1.manageFinish
     (ω : RiverWindowManagerV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 2
 
 def RiverWindowManagerV1.manageDirty
     (ω : RiverWindowManagerV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 3
 
 def RiverWindowManagerV1.renderFinish
     (ω : RiverWindowManagerV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 4
 
 def RiverWindowManagerV1.getShellSurface
     (ω : RiverWindowManagerV1)
     (surface : WlSurface)
     : DisplayM σ RiverShellSurfaceV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .object surface
     return 5
@@ -49,25 +49,25 @@ def RiverWindowManagerV1.getShellSurface
 def RiverWindowManagerV1.exitSession
     (ω : RiverWindowManagerV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 6
 
 def RiverWindowV1.destroy
     (ω : RiverWindowV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def RiverWindowV1.close
     (ω : RiverWindowV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 1
 
 def RiverWindowV1.getNode
     (ω : RiverWindowV1)
     : DisplayM σ RiverNodeV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     return 2
 
@@ -76,7 +76,7 @@ def RiverWindowV1.proposeDimensions
     (width : Int32)
     (height : Int32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .int width
     Marshallable.marshal .int height
     return 3
@@ -84,25 +84,25 @@ def RiverWindowV1.proposeDimensions
 def RiverWindowV1.hide
     (ω : RiverWindowV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 4
 
 def RiverWindowV1.show
     (ω : RiverWindowV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 5
 
 def RiverWindowV1.useCsd
     (ω : RiverWindowV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 6
 
 def RiverWindowV1.useSsd
     (ω : RiverWindowV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 7
 
 def RiverWindowV1.setBorders
@@ -114,7 +114,7 @@ def RiverWindowV1.setBorders
     (b : UInt32)
     (a : UInt32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .uint edges
     Marshallable.marshal .int width
     Marshallable.marshal .uint r
@@ -127,7 +127,7 @@ def RiverWindowV1.setTiled
     (ω : RiverWindowV1)
     (edges : RiverWindowV1.Edges)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .uint edges
     return 9
 
@@ -135,7 +135,7 @@ def RiverWindowV1.getDecorationAbove
     (ω : RiverWindowV1)
     (surface : WlSurface)
     : DisplayM σ RiverDecorationV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .object surface
     return 10
@@ -144,7 +144,7 @@ def RiverWindowV1.getDecorationBelow
     (ω : RiverWindowV1)
     (surface : WlSurface)
     : DisplayM σ RiverDecorationV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .object surface
     return 11
@@ -152,59 +152,59 @@ def RiverWindowV1.getDecorationBelow
 def RiverWindowV1.informResizeStart
     (ω : RiverWindowV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 12
 
 def RiverWindowV1.informResizeEnd
     (ω : RiverWindowV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 13
 
 def RiverWindowV1.setCapabilities
     (ω : RiverWindowV1)
     (caps : RiverWindowV1.Capabilities)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .uint caps
     return 14
 
 def RiverWindowV1.informMaximized
     (ω : RiverWindowV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 15
 
 def RiverWindowV1.informUnmaximized
     (ω : RiverWindowV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 16
 
 def RiverWindowV1.informFullscreen
     (ω : RiverWindowV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 17
 
 def RiverWindowV1.informNotFullscreen
     (ω : RiverWindowV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 18
 
 def RiverWindowV1.fullscreen
     (ω : RiverWindowV1)
     (output : RiverOutputV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .object output
     return 19
 
 def RiverWindowV1.exitFullscreen
     (ω : RiverWindowV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 20
 
 def RiverWindowV1.setClipBox
@@ -214,7 +214,7 @@ def RiverWindowV1.setClipBox
     (width : Int32)
     (height : Int32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .int x
     Marshallable.marshal .int y
     Marshallable.marshal .int width
@@ -228,7 +228,7 @@ def RiverWindowV1.setContentClipBox
     (width : Int32)
     (height : Int32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .int x
     Marshallable.marshal .int y
     Marshallable.marshal .int width
@@ -240,7 +240,7 @@ def RiverWindowV1.setDimensionBounds
     (maxWidth : Int32)
     (maxHeight : Int32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .int maxWidth
     Marshallable.marshal .int maxHeight
     return 23
@@ -248,7 +248,7 @@ def RiverWindowV1.setDimensionBounds
 def RiverDecorationV1.destroy
     (ω : RiverDecorationV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def RiverDecorationV1.setOffset
@@ -256,7 +256,7 @@ def RiverDecorationV1.setOffset
     (x : Int32)
     (y : Int32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .int x
     Marshallable.marshal .int y
     return 1
@@ -264,32 +264,32 @@ def RiverDecorationV1.setOffset
 def RiverDecorationV1.syncNextCommit
     (ω : RiverDecorationV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 2
 
 def RiverShellSurfaceV1.destroy
     (ω : RiverShellSurfaceV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def RiverShellSurfaceV1.getNode
     (ω : RiverShellSurfaceV1)
     : DisplayM σ RiverNodeV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     return 1
 
 def RiverShellSurfaceV1.syncNextCommit
     (ω : RiverShellSurfaceV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 2
 
 def RiverNodeV1.destroy
     (ω : RiverNodeV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def RiverNodeV1.setPosition
@@ -297,7 +297,7 @@ def RiverNodeV1.setPosition
     (x : Int32)
     (y : Int32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .int x
     Marshallable.marshal .int y
     return 1
@@ -305,20 +305,20 @@ def RiverNodeV1.setPosition
 def RiverNodeV1.placeTop
     (ω : RiverNodeV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 2
 
 def RiverNodeV1.placeBottom
     (ω : RiverNodeV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 3
 
 def RiverNodeV1.placeAbove
     (ω : RiverNodeV1)
     (other : RiverNodeV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .object other
     return 4
 
@@ -326,35 +326,35 @@ def RiverNodeV1.placeBelow
     (ω : RiverNodeV1)
     (other : RiverNodeV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .object other
     return 5
 
 def RiverOutputV1.destroy
     (ω : RiverOutputV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def RiverOutputV1.setPresentationMode
     (ω : RiverOutputV1)
     (mode : RiverOutputV1.PresentationMode)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .uint mode
     return 1
 
 def RiverSeatV1.destroy
     (ω : RiverSeatV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def RiverSeatV1.focusWindow
     (ω : RiverSeatV1)
     (window : RiverWindowV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .object window
     return 1
 
@@ -362,26 +362,26 @@ def RiverSeatV1.focusShellSurface
     (ω : RiverSeatV1)
     (shellSurface : RiverShellSurfaceV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .object shellSurface
     return 2
 
 def RiverSeatV1.clearFocus
     (ω : RiverSeatV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 3
 
 def RiverSeatV1.opStartPointer
     (ω : RiverSeatV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 4
 
 def RiverSeatV1.opEnd
     (ω : RiverSeatV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 5
 
 def RiverSeatV1.getPointerBinding
@@ -389,7 +389,7 @@ def RiverSeatV1.getPointerBinding
     (button : UInt32)
     (modifiers : RiverSeatV1.Modifiers)
     : DisplayM σ RiverPointerBindingV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .uint button
     Marshallable.marshal .uint modifiers
@@ -400,7 +400,7 @@ def RiverSeatV1.setXcursorTheme
     (name : String)
     (size : UInt32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .string name
     Marshallable.marshal .uint size
     return 7
@@ -410,7 +410,7 @@ def RiverSeatV1.pointerWarp
     (x : Int32)
     (y : Int32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .int x
     Marshallable.marshal .int y
     return 8
@@ -418,19 +418,19 @@ def RiverSeatV1.pointerWarp
 def RiverPointerBindingV1.destroy
     (ω : RiverPointerBindingV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def RiverPointerBindingV1.enable
     (ω : RiverPointerBindingV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 1
 
 def RiverPointerBindingV1.disable
     (ω : RiverPointerBindingV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 2
 
 end Wayland.Protocols
\ No newline at end of file
diff --git a/lib/Wayland/Protocols/RiverXkbBindingsV1/Requests.lean b/lib/Wayland/Protocols/RiverXkbBindingsV1/Requests.lean
index 691e32e..b224fbb 100644
--- a/lib/Wayland/Protocols/RiverXkbBindingsV1/Requests.lean
+++ b/lib/Wayland/Protocols/RiverXkbBindingsV1/Requests.lean
@@ -9,7 +9,7 @@ variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι]
 def RiverXkbBindingsV1.destroy
     (ω : RiverXkbBindingsV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def RiverXkbBindingsV1.getXkbBinding
@@ -18,7 +18,7 @@ def RiverXkbBindingsV1.getXkbBinding
     (keysym : UInt32)
     (modifiers : RiverSeatV1.Modifiers)
     : DisplayM σ RiverXkbBindingV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     Marshallable.marshal .object seat
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .uint keysym
@@ -29,7 +29,7 @@ def RiverXkbBindingsV1.getSeat
     (ω : RiverXkbBindingsV1)
     (seat : RiverSeatV1)
     : DisplayM σ RiverXkbBindingsSeatV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .object seat
     return 2
@@ -37,45 +37,45 @@ def RiverXkbBindingsV1.getSeat
 def RiverXkbBindingV1.destroy
     (ω : RiverXkbBindingV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def RiverXkbBindingV1.setLayoutOverride
     (ω : RiverXkbBindingV1)
     (layout : UInt32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .uint layout
     return 1
 
 def RiverXkbBindingV1.enable
     (ω : RiverXkbBindingV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 2
 
 def RiverXkbBindingV1.disable
     (ω : RiverXkbBindingV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 3
 
 def RiverXkbBindingsSeatV1.destroy
     (ω : RiverXkbBindingsSeatV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def RiverXkbBindingsSeatV1.ensureNextKeyEaten
     (ω : RiverXkbBindingsSeatV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 1
 
 def RiverXkbBindingsSeatV1.cancelEnsureNextKeyEaten
     (ω : RiverXkbBindingsSeatV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 2
 
 end Wayland.Protocols
\ No newline at end of file
diff --git a/lib/Wayland/Protocols/RiverXkbConfigV1/Requests.lean b/lib/Wayland/Protocols/RiverXkbConfigV1/Requests.lean
index 7cae24d..8e58633 100644
--- a/lib/Wayland/Protocols/RiverXkbConfigV1/Requests.lean
+++ b/lib/Wayland/Protocols/RiverXkbConfigV1/Requests.lean
@@ -9,13 +9,13 @@ variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι]
 def RiverXkbConfigV1.stop
     (ω : RiverXkbConfigV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 0
 
 def RiverXkbConfigV1.destroy
     (ω : RiverXkbConfigV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 1
 
 def RiverXkbConfigV1.createKeymap
@@ -23,7 +23,7 @@ def RiverXkbConfigV1.createKeymap
     (fd : Fd)
     (format : RiverXkbConfigV1.KeymapFormat)
     : DisplayM σ RiverXkbKeymapV1 :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .fd fd
     Marshallable.marshal .uint format
@@ -32,20 +32,20 @@ def RiverXkbConfigV1.createKeymap
 def RiverXkbKeymapV1.destroy
     (ω : RiverXkbKeymapV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def RiverXkbKeyboardV1.destroy
     (ω : RiverXkbKeyboardV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def RiverXkbKeyboardV1.setKeymap
     (ω : RiverXkbKeyboardV1)
     (keymap : RiverXkbKeymapV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .object keymap
     return 1
 
@@ -53,7 +53,7 @@ def RiverXkbKeyboardV1.setLayoutByIndex
     (ω : RiverXkbKeyboardV1)
     (index : Int32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .int index
     return 2
 
@@ -61,32 +61,32 @@ def RiverXkbKeyboardV1.setLayoutByName
     (ω : RiverXkbKeyboardV1)
     (name : String)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .string name
     return 3
 
 def RiverXkbKeyboardV1.capslockEnable
     (ω : RiverXkbKeyboardV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 4
 
 def RiverXkbKeyboardV1.capslockDisable
     (ω : RiverXkbKeyboardV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 5
 
 def RiverXkbKeyboardV1.numlockEnable
     (ω : RiverXkbKeyboardV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 6
 
 def RiverXkbKeyboardV1.numlockDisable
     (ω : RiverXkbKeyboardV1)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 7
 
 end Wayland.Protocols
\ No newline at end of file
diff --git a/lib/Wayland/Protocols/Wayland/Requests.lean b/lib/Wayland/Protocols/Wayland/Requests.lean
index f25082d..1ab15ab 100644
--- a/lib/Wayland/Protocols/Wayland/Requests.lean
+++ b/lib/Wayland/Protocols/Wayland/Requests.lean
@@ -9,7 +9,7 @@ variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι]
 def WlDisplay.sync.raw
     (ω : WlDisplay)
     : DisplayM σ WlCallback :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     return 0
 
@@ -24,7 +24,7 @@ def WlDisplay.sync
 def WlDisplay.getRegistry
     (ω : WlDisplay)
     : DisplayM σ WlRegistry :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     return 1
 
@@ -32,7 +32,7 @@ def WlRegistry.bind
     (ω : WlRegistry)
     (name : UInt32)
     : DisplayM σ (Object ι) :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     Marshallable.marshal .uint name
     ArgumentMarshaller.marshalString (.some ι)
     ArgumentMarshaller.marshalUInt (inferInstance : Interface ι).version
@@ -42,14 +42,14 @@ def WlRegistry.bind
 def WlCompositor.createSurface
     (ω : WlCompositor)
     : DisplayM σ WlSurface :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     return 0
 
 def WlCompositor.createRegion
     (ω : WlCompositor)
     : DisplayM σ WlRegion :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     return 1
 
@@ -61,7 +61,7 @@ def WlShmPool.createBuffer
     (stride : Int32)
     (format : WlShm.Format)
     : DisplayM σ WlBuffer :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .int offset
     Marshallable.marshal .int width
@@ -73,14 +73,14 @@ def WlShmPool.createBuffer
 def WlShmPool.destroy
     (ω : WlShmPool)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 1
 
 def WlShmPool.resize
     (ω : WlShmPool)
     (size : Int32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .int size
     return 2
 
@@ -89,7 +89,7 @@ def WlShm.createPool
     (fd : Fd)
     (size : Int32)
     : DisplayM σ WlShmPool :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .fd fd
     Marshallable.marshal .int size
@@ -98,13 +98,13 @@ def WlShm.createPool
 def WlShm.release
     (ω : WlShm)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 1
 
 def WlBuffer.destroy
     (ω : WlBuffer)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def WlDataOffer.accept
@@ -112,7 +112,7 @@ def WlDataOffer.accept
     (serial : UInt32)
     (mimeType : Option String)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .uint serial
     Marshallable.marshal .string mimeType
     return 0
@@ -122,7 +122,7 @@ def WlDataOffer.receive
     (mimeType : String)
     (fd : Fd)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .string mimeType
     Marshallable.marshal .fd fd
     return 1
@@ -130,13 +130,13 @@ def WlDataOffer.receive
 def WlDataOffer.destroy
     (ω : WlDataOffer)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 2
 
 def WlDataOffer.finish
     (ω : WlDataOffer)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 3
 
 def WlDataOffer.setActions
@@ -144,7 +144,7 @@ def WlDataOffer.setActions
     (dndActions : WlDataDeviceManager.DndAction)
     (preferredAction : WlDataDeviceManager.DndAction)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .uint dndActions
     Marshallable.marshal .uint preferredAction
     return 4
@@ -153,21 +153,21 @@ def WlDataSource.offer
     (ω : WlDataSource)
     (mimeType : String)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .string mimeType
     return 0
 
 def WlDataSource.destroy
     (ω : WlDataSource)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 1
 
 def WlDataSource.setActions
     (ω : WlDataSource)
     (dndActions : WlDataDeviceManager.DndAction)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .uint dndActions
     return 2
 
@@ -178,7 +178,7 @@ def WlDataDevice.startDrag
     (icon : Option WlSurface)
     (serial : UInt32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .object source
     Marshallable.marshal .object origin
     Marshallable.marshal .object icon
@@ -190,7 +190,7 @@ def WlDataDevice.setSelection
     (source : Option WlDataSource)
     (serial : UInt32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .object source
     Marshallable.marshal .uint serial
     return 1
@@ -198,13 +198,13 @@ def WlDataDevice.setSelection
 def WlDataDevice.release
     (ω : WlDataDevice)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 2
 
 def WlDataDeviceManager.createDataSource
     (ω : WlDataDeviceManager)
     : DisplayM σ WlDataSource :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     return 0
 
@@ -212,7 +212,7 @@ def WlDataDeviceManager.getDataDevice
     (ω : WlDataDeviceManager)
     (seat : WlSeat)
     : DisplayM σ WlDataDevice :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .object seat
     return 1
@@ -221,7 +221,7 @@ def WlShell.getShellSurface
     (ω : WlShell)
     (surface : WlSurface)
     : DisplayM σ WlShellSurface :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .object surface
     return 0
@@ -230,7 +230,7 @@ def WlShellSurface.pong
     (ω : WlShellSurface)
     (serial : UInt32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .uint serial
     return 0
 
@@ -239,7 +239,7 @@ def WlShellSurface.move
     (seat : WlSeat)
     (serial : UInt32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .object seat
     Marshallable.marshal .uint serial
     return 1
@@ -250,7 +250,7 @@ def WlShellSurface.resize
     (serial : UInt32)
     (edges : WlShellSurface.Resize)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .object seat
     Marshallable.marshal .uint serial
     Marshallable.marshal .uint edges
@@ -259,7 +259,7 @@ def WlShellSurface.resize
 def WlShellSurface.setToplevel
     (ω : WlShellSurface)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 3
 
 def WlShellSurface.setTransient
@@ -269,7 +269,7 @@ def WlShellSurface.setTransient
     (y : Int32)
     (flags : WlShellSurface.Transient)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .object parent
     Marshallable.marshal .int x
     Marshallable.marshal .int y
@@ -282,7 +282,7 @@ def WlShellSurface.setFullscreen
     (framerate : UInt32)
     (output : Option WlOutput)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .uint method
     Marshallable.marshal .uint framerate
     Marshallable.marshal .object output
@@ -297,7 +297,7 @@ def WlShellSurface.setPopup
     (y : Int32)
     (flags : WlShellSurface.Transient)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .object seat
     Marshallable.marshal .uint serial
     Marshallable.marshal .object parent
@@ -310,7 +310,7 @@ def WlShellSurface.setMaximized
     (ω : WlShellSurface)
     (output : Option WlOutput)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .object output
     return 7
 
@@ -318,7 +318,7 @@ def WlShellSurface.setTitle
     (ω : WlShellSurface)
     (title : String)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .string title
     return 8
 
@@ -326,14 +326,14 @@ def WlShellSurface.setClass
     (ω : WlShellSurface)
     (_class : String)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .string _class
     return 9
 
 def WlSurface.destroy
     (ω : WlSurface)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def WlSurface.attach
@@ -342,7 +342,7 @@ def WlSurface.attach
     (x : Int32)
     (y : Int32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .object buffer
     Marshallable.marshal .int x
     Marshallable.marshal .int y
@@ -355,7 +355,7 @@ def WlSurface.damage
     (width : Int32)
     (height : Int32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .int x
     Marshallable.marshal .int y
     Marshallable.marshal .int width
@@ -365,7 +365,7 @@ def WlSurface.damage
 def WlSurface.frame.raw
     (ω : WlSurface)
     : DisplayM σ WlCallback :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     return 3
 
@@ -381,7 +381,7 @@ def WlSurface.setOpaqueRegion
     (ω : WlSurface)
     (region : Option WlRegion)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .object region
     return 4
 
@@ -389,21 +389,21 @@ def WlSurface.setInputRegion
     (ω : WlSurface)
     (region : Option WlRegion)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .object region
     return 5
 
 def WlSurface.commit
     (ω : WlSurface)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 6
 
 def WlSurface.setBufferTransform
     (ω : WlSurface)
     (transform : WlOutput.Transform)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .int transform
     return 7
 
@@ -411,7 +411,7 @@ def WlSurface.setBufferScale
     (ω : WlSurface)
     (scale : Int32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .int scale
     return 8
 
@@ -422,7 +422,7 @@ def WlSurface.damageBuffer
     (width : Int32)
     (height : Int32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .int x
     Marshallable.marshal .int y
     Marshallable.marshal .int width
@@ -434,7 +434,7 @@ def WlSurface.offset
     (x : Int32)
     (y : Int32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .int x
     Marshallable.marshal .int y
     return 10
@@ -442,28 +442,28 @@ def WlSurface.offset
 def WlSeat.getPointer
     (ω : WlSeat)
     : DisplayM σ WlPointer :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     return 0
 
 def WlSeat.getKeyboard
     (ω : WlSeat)
     : DisplayM σ WlKeyboard :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     return 1
 
 def WlSeat.getTouch
     (ω : WlSeat)
     : DisplayM σ WlTouch :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     return 2
 
 def WlSeat.release
     (ω : WlSeat)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 3
 
 def WlPointer.setCursor
@@ -473,7 +473,7 @@ def WlPointer.setCursor
     (hotspotX : Int32)
     (hotspotY : Int32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .uint serial
     Marshallable.marshal .object surface
     Marshallable.marshal .int hotspotX
@@ -483,31 +483,31 @@ def WlPointer.setCursor
 def WlPointer.release
     (ω : WlPointer)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 1
 
 def WlKeyboard.release
     (ω : WlKeyboard)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def WlTouch.release
     (ω : WlTouch)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def WlOutput.release
     (ω : WlOutput)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def WlRegion.destroy
     (ω : WlRegion)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def WlRegion.add
@@ -517,7 +517,7 @@ def WlRegion.add
     (width : Int32)
     (height : Int32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .int x
     Marshallable.marshal .int y
     Marshallable.marshal .int width
@@ -531,7 +531,7 @@ def WlRegion.subtract
     (width : Int32)
     (height : Int32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .int x
     Marshallable.marshal .int y
     Marshallable.marshal .int width
@@ -541,7 +541,7 @@ def WlRegion.subtract
 def WlSubcompositor.destroy
     (ω : WlSubcompositor)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def WlSubcompositor.getSubsurface
@@ -549,7 +549,7 @@ def WlSubcompositor.getSubsurface
     (surface : WlSurface)
     (parent : WlSurface)
     : DisplayM σ WlSubsurface :=
-  ω.sendConstructor do
+  ω.sendConstructor false do
     ArgumentMarshaller.marshalAnyObject .none
     Marshallable.marshal .object surface
     Marshallable.marshal .object parent
@@ -558,7 +558,7 @@ def WlSubcompositor.getSubsurface
 def WlSubsurface.destroy
     (ω : WlSubsurface)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def WlSubsurface.setPosition
@@ -566,7 +566,7 @@ def WlSubsurface.setPosition
     (x : Int32)
     (y : Int32)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .int x
     Marshallable.marshal .int y
     return 1
@@ -575,7 +575,7 @@ def WlSubsurface.placeAbove
     (ω : WlSubsurface)
     (sibling : WlSurface)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .object sibling
     return 2
 
@@ -583,33 +583,33 @@ def WlSubsurface.placeBelow
     (ω : WlSubsurface)
     (sibling : WlSurface)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .object sibling
     return 3
 
 def WlSubsurface.setSync
     (ω : WlSubsurface)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 4
 
 def WlSubsurface.setDesync
     (ω : WlSubsurface)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     return 5
 
 def WlFixes.destroy
     (ω : WlFixes)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send true do
     return 0
 
 def WlFixes.destroyRegistry
     (ω : WlFixes)
     (registry : WlRegistry)
     : DisplayM σ Unit :=
-  ω.send do
+  ω.send false do
     Marshallable.marshal .object registry
     return 1
 
diff --git a/src/Waylean.lean b/src/Waylean.lean
index 0f0a2e1..e47c6ad 100644
--- a/src/Waylean.lean
+++ b/src/Waylean.lean
@@ -230,18 +230,19 @@ def Seat.opEnd (s : Seat) : DisplayM State Seat := do
   s.proxy.opEnd
   return { s with op := .none }
 
-def Seat.opManage (s : Seat) : DisplayM State Seat := do
+def Seat.opManage (s : Seat) : DisplayM State Unit := do
   match s.op with
-    | .resize proxy startX startY startWidth startHeight edges =>
+    | .resize proxy _ _ startWidth startHeight edges =>
         let mut width := startWidth
         let mut height := startHeight
         if edges.left   then width  := width  - s.opDeltaX
         if edges.right  then width  := width  + s.opDeltaX
         if edges.top    then height := height - s.opDeltaY
         if edges.bottom then height := height + s.opDeltaY
+        width  := if width  > 0 then width  else 1
+        height := if height > 0 then height else 1
         proxy.proposeDimensions width height
-        pure { s with op := .resize proxy startX startY width height edges }
-    | _ => pure s
+    | _ => pure ()
 
 def removeOutputs : DisplayM State Unit := do
   let (removedOutputs, aliveOutputs) := (← get).outputs.partition fun _ out ↦ out.removed
@@ -256,16 +257,16 @@ def removeWindows : DisplayM State Unit := do
     seats ← seats.mapM fun _ seat ↦ do
       let op  ← match seat.op with
         | .none => pure SeatOp.none
-        | .move proxy startX startY =>
+        | op@(.move proxy _ _) =>
             if proxy == win.proxy then
               seat.proxy.opEnd
               pure SeatOp.none
-            else pure (SeatOp.move proxy startX startY)
-        | .resize proxy startX startY startWidth startHeight edges =>
+            else pure op
+        | op@(.resize proxy _ _ _ _ _) =>
             if proxy == win.proxy then
               seat.proxy.opEnd
               pure SeatOp.none
-            else pure (SeatOp.resize proxy startX startY startWidth startHeight edges)
+            else pure op
       pure { seat with
         op
         focused := if seat.focused == win.proxy then .none else seat.focused
@@ -347,7 +348,7 @@ def manageSeats (ctx : Context) : DisplayM State Unit := do
     if seat.opRelease then
       seat ← seat.opEnd
     else
-      seat ← seat.opManage
+      seat.opManage
     pure { seat with
       interacted := .none
       opRelease := false
@@ -370,15 +371,14 @@ def handle (ctx : Context) : RiverWindowManagerV1.Event → DisplayM State Unit
       manageSeats ctx
       ctx.wm.manageFinish
   | .renderStart => do
-      let seats ←  (← get).seats.mapM fun _ seat ↦ do
+      for seat in (← get).seats.values do
         match seat.op with
-          | .none => pure seat
+          | .none => pure ()
           | .move proxy startX startY =>
               let windows ← (← get).windows.findAndModifyM
                 (fun win ↦ win.proxy == proxy)
                 (fun win ↦ win.setPosition (startX + seat.opDeltaX) (startY + seat.opDeltaY))
               set { ← get with windows := windows.fst }
-              pure seat
           | .resize proxy startX startY startWidth startHeight edges =>
               let windows ← (← get).windows.findAndModifyM
                 (fun win ↦ win.proxy == proxy)
@@ -387,10 +387,6 @@ def handle (ctx : Context) : RiverWindowManagerV1.Event → DisplayM State Unit
                   let y := startY + if edges.top then (startHeight - win.height) else 0
                   win.setPosition x y)
               set { ← get with windows := windows.fst }
-              match windows.snd with
-                | .none => pure seat
-                | .some win => pure { seat with op := .resize proxy win.x win.y startWidth startHeight edges }
-      set { ← get with seats }
       ctx.wm.renderFinish
   | .sessionLocked => pure ()
   | .sessionUnlocked => pure ()
diff --git a/tools/Scanner/Generator.lean b/tools/Scanner/Generator.lean
index 2fa4fdd..525f1d7 100644
--- a/tools/Scanner/Generator.lean
+++ b/tools/Scanner/Generator.lean
@@ -281,8 +281,8 @@ private def emitRequests (protocol : ProtocolDesc) : Generator Unit := do
         | .object .none         => emitLine s!"    : DisplayM σ (Object ι) :="
         | .object (.some iface) => emitLine s!"    : DisplayM σ {← resolveInterface iface (suffix := ".Resolved")} :="
       match req.returnType with
-        | .unit     => emitLine s!"  ω.send do"
-        | .object _ => emitLine s!"  ω.sendConstructor do"
+        | .unit     => emitLine s!"  ω.send {req.isDestructor} do"
+        | .object _ => emitLine s!"  ω.sendConstructor {req.isDestructor} do"
       for arg in req.arguments do
         match arg.type with
           | .newID (.some _) =>