1 files changed, 22 insertions, 3 deletions
diff --git a/tools/Scanner.lean b/tools/Scanner.lean
index 81b4181..1daed2a 100644
--- a/tools/Scanner.lean
+++ b/tools/Scanner.lean
@@ -1,6 +1,7 @@
 import Scanner.Protocol
 import Scanner.Parser
 import Scanner.Processor
+import Scanner.Generator
 
 open WaylandScanner
 
@@ -9,6 +10,24 @@ def parseRawProtocol (path : System.FilePath) : IO Raw.ProtocolDesc := do
     |>.mapError (fun ε ↦ s!"{path}: {ε}")
     |> IO.ofExcept
 
+def writeProtocol (protocol : Client.ProtocolDesc) (rootModule : String) (rootModulePath : System.FilePath) : IO Unit := do
+  let protocolPath := rootModulePath / protocol.name.pascalCase
+  IO.FS.createDirAll protocolPath
+  let umbrellaPath := protocolPath.addExtension "lean"
+  IO.FS.writeFile umbrellaPath <| generateUmbrella rootModule protocol
+  let headerPath := protocolPath / "Header.lean"
+  IO.FS.writeFile headerPath <| generateHeader rootModule protocol
+  let interfacePath := protocolPath / "Interface.lean"
+  IO.FS.writeFile interfacePath <| generateInterface rootModule protocol
+  let resolvedPath := protocolPath / "Resolved.lean"
+  IO.FS.writeFile resolvedPath <| generateResolved rootModule protocol
+  let requestsPath := protocolPath / "Requests.lean"
+  IO.FS.writeFile requestsPath <| generateRequests rootModule protocol
+
+def writeIndex (protocols : Array Client.ProtocolDesc) (rootModule : String) (rootModulePath : System.FilePath) : IO Unit := do
+  let indexPath := rootModulePath.addExtension "lean"
+  IO.FS.writeFile indexPath <| generateIndex rootModule protocols
+
 def process (rootModule : String) (outPath : System.FilePath) (srcPath : System.FilePath) : IO UInt32 := do
   let rawProtocols ← (← srcPath.readDir)
     |>.map IO.FS.DirEntry.path
@@ -19,10 +38,10 @@ def process (rootModule : String) (outPath : System.FilePath) (srcPath : System.
     |>.map String.Slice.toString
     |>.toArray
   let rootModulePath := rootModuleComponents.foldl (· / ·) outPath
-  IO.println (reprStr clientProtocols)
   IO.FS.createDirAll rootModulePath
-  let indexPath := rootModulePath.addExtension "lean"
-  IO.FS.writeFile indexPath ""
+  for protocol in clientProtocols do
+    writeProtocol protocol rootModule rootModulePath
+  writeIndex clientProtocols rootModule rootModulePath
   return 0
 
 def usage : IO UInt32 := do