diff options
Diffstat (limited to 'lib/Wayland/Protocols/RiverWindowManagementV1/Requests.lean')
| -rw-r--r-- | lib/Wayland/Protocols/RiverWindowManagementV1/Requests.lean | 436 |
1 files changed, 436 insertions, 0 deletions
diff --git a/lib/Wayland/Protocols/RiverWindowManagementV1/Requests.lean b/lib/Wayland/Protocols/RiverWindowManagementV1/Requests.lean new file mode 100644 index 0000000..ed70fed --- /dev/null +++ b/lib/Wayland/Protocols/RiverWindowManagementV1/Requests.lean @@ -0,0 +1,436 @@ +import Wayland.Display +import Wayland.Protocols.RiverWindowManagementV1.Header +import Wayland.Protocols.RiverWindowManagementV1.Resolved +import Wayland.Protocols.Wayland.Header + +namespace Wayland.Protocols + +variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι] + +def RiverWindowManagerV1.stop + (ω : RiverWindowManagerV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverWindowManagerV1.destroy + (ω : RiverWindowManagerV1) + : DisplayM σ Unit := + ω.send do + return 1 + +def RiverWindowManagerV1.manageFinish + (ω : RiverWindowManagerV1) + : DisplayM σ Unit := + ω.send do + return 2 + +def RiverWindowManagerV1.manageDirty + (ω : RiverWindowManagerV1) + : DisplayM σ Unit := + ω.send do + return 3 + +def RiverWindowManagerV1.renderFinish + (ω : RiverWindowManagerV1) + : DisplayM σ Unit := + ω.send do + return 4 + +def RiverWindowManagerV1.getShellSurface + (ω : RiverWindowManagerV1) + (surface : WlSurface) + : DisplayM σ RiverShellSurfaceV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .object surface + return 5 + +def RiverWindowManagerV1.exitSession + (ω : RiverWindowManagerV1) + : DisplayM σ Unit := + ω.send do + return 6 + +def RiverWindowV1.destroy + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverWindowV1.close + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 1 + +def RiverWindowV1.getNode + (ω : RiverWindowV1) + : DisplayM σ RiverNodeV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + return 2 + +def RiverWindowV1.proposeDimensions + (ω : RiverWindowV1) + (width : Int32) + (height : Int32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .int width + Marshallable.marshal .int height + return 3 + +def RiverWindowV1.hide + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 4 + +def RiverWindowV1.show + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 5 + +def RiverWindowV1.useCsd + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 6 + +def RiverWindowV1.useSsd + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 7 + +def RiverWindowV1.setBorders + (ω : RiverWindowV1) + (edges : RiverWindowV1.Edges) + (width : Int32) + (r : UInt32) + (g : UInt32) + (b : UInt32) + (a : UInt32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .uint edges + Marshallable.marshal .int width + Marshallable.marshal .uint r + Marshallable.marshal .uint g + Marshallable.marshal .uint b + Marshallable.marshal .uint a + return 8 + +def RiverWindowV1.setTiled + (ω : RiverWindowV1) + (edges : RiverWindowV1.Edges) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .uint edges + return 9 + +def RiverWindowV1.getDecorationAbove + (ω : RiverWindowV1) + (surface : WlSurface) + : DisplayM σ RiverDecorationV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .object surface + return 10 + +def RiverWindowV1.getDecorationBelow + (ω : RiverWindowV1) + (surface : WlSurface) + : DisplayM σ RiverDecorationV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .object surface + return 11 + +def RiverWindowV1.informResizeStart + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 12 + +def RiverWindowV1.informResizeEnd + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 13 + +def RiverWindowV1.setCapabilities + (ω : RiverWindowV1) + (caps : RiverWindowV1.Capabilities) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .uint caps + return 14 + +def RiverWindowV1.informMaximized + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 15 + +def RiverWindowV1.informUnmaximized + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 16 + +def RiverWindowV1.informFullscreen + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 17 + +def RiverWindowV1.informNotFullscreen + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 18 + +def RiverWindowV1.fullscreen + (ω : RiverWindowV1) + (output : RiverOutputV1) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object output + return 19 + +def RiverWindowV1.exitFullscreen + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 20 + +def RiverWindowV1.setClipBox + (ω : RiverWindowV1) + (x : Int32) + (y : Int32) + (width : Int32) + (height : Int32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .int x + Marshallable.marshal .int y + Marshallable.marshal .int width + Marshallable.marshal .int height + return 21 + +def RiverWindowV1.setContentClipBox + (ω : RiverWindowV1) + (x : Int32) + (y : Int32) + (width : Int32) + (height : Int32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .int x + Marshallable.marshal .int y + Marshallable.marshal .int width + Marshallable.marshal .int height + return 22 + +def RiverWindowV1.setDimensionBounds + (ω : RiverWindowV1) + (maxWidth : Int32) + (maxHeight : Int32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .int maxWidth + Marshallable.marshal .int maxHeight + return 23 + +def RiverDecorationV1.destroy + (ω : RiverDecorationV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverDecorationV1.setOffset + (ω : RiverDecorationV1) + (x : Int32) + (y : Int32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .int x + Marshallable.marshal .int y + return 1 + +def RiverDecorationV1.syncNextCommit + (ω : RiverDecorationV1) + : DisplayM σ Unit := + ω.send do + return 2 + +def RiverShellSurfaceV1.destroy + (ω : RiverShellSurfaceV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverShellSurfaceV1.getNode + (ω : RiverShellSurfaceV1) + : DisplayM σ RiverNodeV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + return 1 + +def RiverShellSurfaceV1.syncNextCommit + (ω : RiverShellSurfaceV1) + : DisplayM σ Unit := + ω.send do + return 2 + +def RiverNodeV1.destroy + (ω : RiverNodeV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverNodeV1.setPosition + (ω : RiverNodeV1) + (x : Int32) + (y : Int32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .int x + Marshallable.marshal .int y + return 1 + +def RiverNodeV1.placeTop + (ω : RiverNodeV1) + : DisplayM σ Unit := + ω.send do + return 2 + +def RiverNodeV1.placeBottom + (ω : RiverNodeV1) + : DisplayM σ Unit := + ω.send do + return 3 + +def RiverNodeV1.placeAbove + (ω : RiverNodeV1) + (other : RiverNodeV1) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object other + return 4 + +def RiverNodeV1.placeBelow + (ω : RiverNodeV1) + (other : RiverNodeV1) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object other + return 5 + +def RiverOutputV1.destroy + (ω : RiverOutputV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverOutputV1.setPresentationMode + (ω : RiverOutputV1) + (mode : RiverOutputV1.PresentationMode) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .uint mode + return 1 + +def RiverSeatV1.destroy + (ω : RiverSeatV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverSeatV1.focusWindow + (ω : RiverSeatV1) + (window : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object window + return 1 + +def RiverSeatV1.focusShellSurface + (ω : RiverSeatV1) + (shellSurface : RiverShellSurfaceV1) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object shellSurface + return 2 + +def RiverSeatV1.clearFocus + (ω : RiverSeatV1) + : DisplayM σ Unit := + ω.send do + return 3 + +def RiverSeatV1.opStartPointer + (ω : RiverSeatV1) + : DisplayM σ Unit := + ω.send do + return 4 + +def RiverSeatV1.opEnd + (ω : RiverSeatV1) + : DisplayM σ Unit := + ω.send do + return 5 + +def RiverSeatV1.getPointerBinding + (ω : RiverSeatV1) + (button : UInt32) + (modifiers : RiverSeatV1.Modifiers) + : DisplayM σ RiverPointerBindingV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint button + Marshallable.marshal .uint modifiers + return 6 + +def RiverSeatV1.setXcursorTheme + (ω : RiverSeatV1) + (name : String) + (size : UInt32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .string name + Marshallable.marshal .uint size + return 7 + +def RiverSeatV1.pointerWarp + (ω : RiverSeatV1) + (x : Int32) + (y : Int32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .int x + Marshallable.marshal .int y + return 8 + +def RiverPointerBindingV1.destroy + (ω : RiverPointerBindingV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverPointerBindingV1.enable + (ω : RiverPointerBindingV1) + : DisplayM σ Unit := + ω.send do + return 1 + +def RiverPointerBindingV1.disable + (ω : RiverPointerBindingV1) + : DisplayM σ Unit := + ω.send do + return 2 + +end Wayland.Protocols
\ No newline at end of file |