import Wayland.Display
import Wayland.Protocols.RiverLayerShellV1.Resolved
import Wayland.Protocols.RiverWindowManagementV1.Header

namespace Wayland.Protocols

variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι]

def RiverLayerShellV1.destroy
    (ω : RiverLayerShellV1)
    : DisplayM σ Unit :=
  ω.send true do
    return 0

def RiverLayerShellV1.getOutput
    (ω : RiverLayerShellV1)
    (output : RiverOutputV1)
    : DisplayM σ RiverLayerShellOutputV1 :=
  ω.sendConstructor false do
    ArgumentMarshaller.marshalAnyObject .none
    Marshallable.marshal .object output
    return 1

def RiverLayerShellV1.getSeat
    (ω : RiverLayerShellV1)
    (seat : RiverSeatV1)
    : DisplayM σ RiverLayerShellSeatV1 :=
  ω.sendConstructor false do
    ArgumentMarshaller.marshalAnyObject .none
    Marshallable.marshal .object seat
    return 2

def RiverLayerShellOutputV1.destroy
    (ω : RiverLayerShellOutputV1)
    : DisplayM σ Unit :=
  ω.send true do
    return 0

def RiverLayerShellOutputV1.setDefault
    (ω : RiverLayerShellOutputV1)
    : DisplayM σ Unit :=
  ω.send false do
    return 1

def RiverLayerShellSeatV1.destroy
    (ω : RiverLayerShellSeatV1)
    : DisplayM σ Unit :=
  ω.send true do
    return 0

end Wayland.Protocols