diff options
Diffstat (limited to 'lib/Wayland/Display.lean')
| -rw-r--r-- | lib/Wayland/Display.lean | 40 |
1 files changed, 24 insertions, 16 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 |