fix generic new_ids

1 files changed, 8 insertions, 5 deletions

diff --git a/tools/Scanner/Processor.lean b/tools/Scanner/Processor.lean
index a50767f..fd952a2 100644
--- a/tools/Scanner/Processor.lean
+++ b/tools/Scanner/Processor.lean
@@ -87,14 +87,13 @@ private def processArgument (raw : Raw.ArgumentDesc) : TrackingProcessor Client.
         | .string => Client.ArgumentType.string (.ofAllowNull raw.allowNull) |> pure
         | .array  => Client.ArgumentType.array |> pure
         | .fd     => Client.ArgumentType.fd |> pure
-        | .newID  => Client.ArgumentType.object .notNull <$> raw.interface.mapM resolveInterface
+        | .newID  => Client.ArgumentType.newID <$> raw.interface.mapM resolveInterface
         | .object => Client.ArgumentType.object (.ofAllowNull raw.allowNull) <$> raw.interface.mapM resolveInterface
     description := raw.description
   }
 
 private def processRequest (raw : Raw.MessageDesc) : TrackingProcessor Client.RequestDesc := do
   let newIDArgs := raw.arguments.filter fun arg ↦ arg.type == .newID
-  let otherArgs := raw.arguments.filter fun arg ↦ arg.type != .newID
   let returnType ←
     match newIDArgs with
       | #[]    => Client.ReturnType.unit |> pure
@@ -107,12 +106,17 @@ private def processRequest (raw : Raw.MessageDesc) : TrackingProcessor Client.Re
     isDestructor := raw.type == .destructor
     since := raw.since
     deprecatedSince := raw.deprecatedSince
-    rawArguments := raw.arguments
-    arguments := ← otherArgs.mapM processArgument
+    arguments := ← raw.arguments.mapM processArgument
     returnType := returnType
   }
 
 private def processEvent (raw : Raw.MessageDesc) : TrackingProcessor Client.EventDesc := do
+  let hasInvalidArg := raw.arguments.any fun arg ↦
+    match arg.type, arg.interface with
+      | .newID, .none => true
+      | _,      _     => false
+  if hasInvalidArg then
+    throw s!"Event arguments of type new_id must have an interface type specified (in {raw.name})"
   return {
     name := raw.name
     opcode := raw.opcode
@@ -120,7 +124,6 @@ private def processEvent (raw : Raw.MessageDesc) : TrackingProcessor Client.Even
     isDestructor := raw.type == .destructor
     since := raw.since
     deprecatedSince := raw.deprecatedSince
-    rawArguments := raw.arguments
     arguments := ← raw.arguments.mapM processArgument
   }