summaryrefslogtreecommitdiff
path: root/lib/Wayland
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Wayland')
-rw-r--r--lib/Wayland/Display.lean40
-rw-r--r--lib/Wayland/Native.lean7
-rw-r--r--lib/Wayland/Protocols/RiverInputManagementV1/Requests.lean20
-rw-r--r--lib/Wayland/Protocols/RiverLayerShellV1/Requests.lean12
-rw-r--r--lib/Wayland/Protocols/RiverLibinputConfigV1/Requests.lean54
-rw-r--r--lib/Wayland/Protocols/RiverWindowManagementV1/Requests.lean114
-rw-r--r--lib/Wayland/Protocols/RiverXkbBindingsV1/Requests.lean20
-rw-r--r--lib/Wayland/Protocols/RiverXkbConfigV1/Requests.lean24
-rw-r--r--lib/Wayland/Protocols/Wayland/Requests.lean136
9 files changed, 219 insertions, 208 deletions
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
generated by cgit v1.3.1 (git 2.54.0) at 2026-11-10 14:28:44 +0000