diff options
Diffstat (limited to 'lib/Wayland/Display.lean')
| -rw-r--r-- | lib/Wayland/Display.lean | 23 |
1 files changed, 13 insertions, 10 deletions
diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean index 3cfa679..d82a951 100644 --- a/lib/Wayland/Display.lean +++ b/lib/Wayland/Display.lean @@ -34,12 +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 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 deriving Nonempty /-- Monad in which arguments can be marshalled one after another. -/ @@ -278,11 +280,12 @@ private instance : ArgumentDemarshaller (ExceptT String ArgumentBufferM) where demarshalString := do (← read).readString demarshalObject := do let proxy ← (← read).readObject - return proxy.map Object.mk + proxy.mapM fun proxy ↦ do + return ⟨proxy, ← proxy.getID⟩ demarshalAnyObject := do let proxy ← (← read).readObject proxy.mapM fun proxy ↦ do - return ⟨proxy, ← proxy.getType⟩ + return ⟨proxy, ← proxy.getType, ← proxy.getID⟩ demarshalArray := do (← read).readArray demarshalFd := do (← read).readFd @@ -412,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⟩ + return ⟨proxy, ← proxy.getID⟩ variable {ι ι' : InterfaceName} instance : BEq (Object ι) where - beq x y := x.proxy.isEqual y.proxy + beq x y := x.id == y.id instance : Hashable (Object ι) where - hash x := x.proxy.hash + hash x := x.id instance : BEq AnyObject where - beq x y := x.proxy.isEqual y.proxy + beq x y := x.id == y.id instance : Hashable AnyObject where - hash x := x.proxy.hash + hash x := x.id private def marshalArguments (marshaller : ∀ {α} [ArgumentMarshaller α], α OpCode) : IO (Native.ArgumentBuffer × OpCode) := do let argBuffer ← Native.ArgumentBuffer.new @@ -445,7 +448,7 @@ def Object.sendConstructor [iface : ResolvedInterface ι'] (obj : Object ι) (ma let typeMap := (← read).typeMap let (argBuffer, opcode) ← marshalArguments marshaller let proxy ← obj.proxy.sendConstructor opcode argBuffer typeMap ι' - return ⟨proxy⟩ + return ⟨proxy, ← proxy.getID⟩ /-- Listen for events from the server for an object. -/ def Object.listen [iface : Interface ι] (obj : Object ι) (handler : iface.event → DisplayM σ Unit) : DisplayM σ Unit := do @@ -462,11 +465,11 @@ def Object.keep (obj : Object ι) : DisplayM σ Unit := /-- Erase the type information from an object. -/ def Object.toAny (obj : Object ι) : AnyObject := - ⟨obj.proxy, ι⟩ + ⟨obj.proxy, ι, obj.id⟩ /-- 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⟩ else .none + if obj.type == ι then .some ⟨obj.proxy, obj.id⟩ else .none end Proxies |