diff options
Diffstat (limited to 'lib/Wayland/Protocols')
7 files changed, 190 insertions, 190 deletions
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 |