diff options
Diffstat (limited to 'lib/Wayland')
| -rw-r--r-- | lib/Wayland/Native.lean | 39 |
1 files changed, 29 insertions, 10 deletions
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean index d2c3e33..95d1739 100644 --- a/lib/Wayland/Native.lean +++ b/lib/Wayland/Native.lean @@ -1,3 +1,18 @@ +namespace Wayland.Native + +@[extern "waylean_SIGINT"] +private opaque _SIGINT (u : Unit) : UInt32 + +@[extern "waylean_SIGUSR1"] +private opaque _SIGUSR1 (u : Unit) : UInt32 + +@[extern "waylean_SIGUSR2"] +private opaque _SIGUSR2 (u : Unit) : UInt32 + +def SIGINT: UInt32 := _SIGINT () +def SIGUSR1: UInt32 := _SIGUSR1 () +def SIGUSR2: UInt32 := _SIGUSR2 () + private opaque DisplayP : NonemptyType def Display : Type := DisplayP.type instance : Nonempty Display := DisplayP.property @@ -8,31 +23,35 @@ opaque Display.new : (name : @& Option String) → IO Display @[extern "waylean_display_roundtrip"] opaque Display.roundtrip : (display : @& Display) → IO Unit -private opaque EventLoopP : NonemptyType -def EventLoop : Type := EventLoopP.type -instance : Nonempty EventLoop := EventLoopP.property +variable {M : Type} + +private opaque EventLoopP (M : Type) : NonemptyType +def EventLoop (M : Type) : Type := (EventLoopP M).type +instance : Nonempty (EventLoop M) := (EventLoopP M).property private opaque EventSourceP : NonemptyType def EventSource : Type := EventSourceP.type instance : Nonempty EventSource := EventSourceP.property @[extern "waylean_event_loop_new"] -opaque EventLoop.new : IO EventLoop +opaque EventLoop.new : IO (EventLoop M) @[extern "waylean_event_loop_add_display"] -opaque EventLoop.addDisplay : (eventLoop : @& EventLoop) → (display : @& Display) → IO EventSource +opaque EventLoop.addDisplay : (eventLoop : @& (EventLoop M)) → (display : @& Display) → IO EventSource @[extern "waylean_event_loop_add_timer"] -opaque EventLoop.addTimer : (eventLoop : @& EventLoop) → (delayMs : UInt32) → (msg : @& IO Unit) → IO EventSource +opaque EventLoop.addTimer : (eventLoop : @& (EventLoop M)) → (delayMs : UInt32) → (msg : @& M) → IO EventSource @[extern "waylean_event_loop_add_signal"] -opaque EventLoop.addSignal : (eventLoop : @& EventLoop) → (signum : UInt32) → (msg : @& IO Unit) → IO EventSource +opaque EventLoop.addSignal : (eventLoop : @& (EventLoop M)) → (signum : UInt32) → (msg : @& M) → IO EventSource @[extern "waylean_event_loop_remove"] -opaque EventLoop.remove : (eventLoop : @& EventLoop) → (source : @& EventSource) → IO Unit +opaque EventLoop.remove : (eventLoop : @& (EventLoop M)) → (source : @& EventSource) → IO Unit @[extern "waylean_event_loop_quit"] -opaque EventLoop.quit : (eventLoop : @& EventLoop) → IO Unit +opaque EventLoop.quit : (eventLoop : @& (EventLoop M)) → IO Unit @[extern "waylean_event_loop_poll"] -opaque EventLoop.poll : (eventLoop : @& EventLoop) → IO (Option (IO Unit)) +opaque EventLoop.poll : (eventLoop : @& (EventLoop M)) → IO (Option M) + +end Wayland.Native |