1 files changed, 6 insertions, 63 deletions
diff --git a/src/Waylean.lean b/src/Waylean.lean
index b595672..f7eb668 100644
--- a/src/Waylean.lean
+++ b/src/Waylean.lean
@@ -1,67 +1,10 @@
 import Wayland
-open Wayland
+open Wayland Protocols
 
-
-def WLCallback.name : InterfaceName := "wl_callback"
-def WLDisplay.name : InterfaceName := "wl_display"
-
-def WLDisplay : Type := Object WLDisplay.name
-def WLCallback : Type := Object WLCallback.name
-
-inductive WLDisplay.Event where
-  | error : (code : UInt32) → (message : String) → Event
-
-instance : Interface WLDisplay.name where
-  event := WLDisplay.Event
-  requests :=
-    #[ { name := "sync"
-         args := #[.newID WLCallback.name]
-         since := 0
-         isDestructor := False } ]
-  events :=
-    #[ { name := "error"
-         args := #[.object .notNull WLDisplay.name, .uint, .string .notNull]
-         since := 0
-         isDestructor := False } ]
-  demarshalEvent
-    | 0 => do
-      (_ : Option (Object WLDisplay.name)) ← ArgumentDemarshaller.demarshalObject
-      return .error
-        (← ArgumentDemarshaller.demarshalUInt)
-        ((← ArgumentDemarshaller.demarshalString).getD "")
-    | _ => sorry
-  version := 1
-
-inductive WLCallback.Event where
-  | done : (data : UInt32) → Event
-
-instance : Interface WLCallback.name where
-  event := WLCallback.Event
-  requests :=
-    #[]
-  events :=
-    #[ { name := "done"
-         args := #[.uint]
-         since := 0
-         isDestructor := False } ]
-  demarshalEvent
-    | 0 => do
-      return .done
-        (← ArgumentDemarshaller.demarshalUInt)
-    | _ => sorry
-  version := 1
-
-instance : ResolvedInterface WLDisplay.name where
-  referencedInterfaces := #[⟨WLDisplay.name, inferInstance⟩, ⟨WLCallback.name, inferInstance⟩]
-
-instance : ResolvedInterface WLCallback.name where
-  referencedInterfaces := #[⟨WLCallback.name, inferInstance⟩]
-
-def WLDisplay.sync {σ : Type} (display : WLDisplay) (handler : DisplayM σ Unit) : DisplayM σ Unit := do
-  let callback : WLCallback ← display.sendConstructor do
-    return 0
+def Wayland.Protocols.WlDisplay.roundtrip {σ : Type} (display : WlDisplay) (handler : DisplayM σ Unit) : DisplayM σ Unit := do
+  let callback ← display.sync
   callback.listen fun
-  | .done _ => do
+    | .done _ => do
       callback.keep
       handler
 
@@ -81,8 +24,8 @@ def launch : DisplayM State Unit := do
     DisplayM.requestQuit
   DisplayM.zoom (mk_lens count) nextTimer
 
-  let disp : WLDisplay ← DisplayM.getDisplay
-  disp.sync do
+  let disp : WlDisplay ← DisplayM.getDisplay
+  disp.roundtrip do
     DisplayM.liftIO (IO.println "Roundtrip complete")
 
 def main : IO Unit :=