From 8eb2236827a89286169276382fdd202994d92f5f Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 16 Jun 2022 22:41:58 +0200
Subject: [PATCH] chore: adapt to `where` syntax change

---
 Lake/DSL/Package.lean | 6 +++---
 Lake/DSL/Targets.lean | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/Lake/DSL/Package.lean b/Lake/DSL/Package.lean
index cbe4c65..010d046 100644
--- a/Lake/DSL/Package.lean
+++ b/Lake/DSL/Package.lean
@@ -42,15 +42,15 @@ def mkPackageDecl (doc? : Option Syntax) (attrs : Array Syntax) : Macro
 | `(packageDeclSpec| $id:ident) =>
   `($[$doc?:docComment]? @[$attrs,*] def $(mkIdentFrom id packageDeclName) : PackageConfig :=
     {name := $(quote id.getId)})
-| `(packageDeclSpec| $id:ident where $[$ds]* $[$wds?]?) =>
+| `(packageDeclSpec| $id:ident where $ds;* $[$wds?]?) =>
   `($[$doc?:docComment]? @[$attrs,*] def $(mkIdentFrom id packageDeclName) : PackageConfig where
-      name := $(quote id.getId) $[$ds]* $[$wds?]?)
+      name := $(quote id.getId); $ds;* $[$wds?]?)
 | `(packageDeclSpec| $id:ident : $ty := $defn $[$wds?]?) =>
   `($[$doc?:docComment]? @[$attrs,*] def $(mkIdentFrom id packageDeclName) : $ty := $defn $[$wds?]?)
 | `(packageDeclSpec| $id:ident $[($dir?)]? $[($args?)]? := $defn $[$wds?]?) =>
   mkSimplePackageDecl doc? attrs (mkIdentFrom id packageDeclName) defn dir? args? wds?
 | `(packageDeclSpec| $id:ident $[($dir?)]? $[($args?)]? { $[$fs $[,]?]* } $[$wds?]?) => do
-  let defn ← `({ name := $(quote id.getId), $[$fs]* })
+  let defn ← `({ name := $(quote id.getId), $fs,* })
   mkSimplePackageDecl doc? attrs (mkIdentFrom id packageDeclName) defn dir? args? wds?
 | `(packageDeclSpec| $id:ident $[($dir?)]? $[($args?)]? do $seq $[$wds?]?) => do
   let (_, dir, args) ← expandPackageBinders dir? args?
diff --git a/Lake/DSL/Targets.lean b/Lake/DSL/Targets.lean
index e283a66..7bfaef7 100644
--- a/Lake/DSL/Targets.lean
+++ b/Lake/DSL/Targets.lean
@@ -23,13 +23,13 @@ def mkTargetDecl
 | `(targetDeclSpec| $id:ident) =>
   `($[$doc?:docComment]? @[$attrs,*] def $id : $ty :=
     {name := $(quote id.getId)})
-| `(targetDeclSpec| $id:ident where $[$ds]* $[$wds?]?) =>
+| `(targetDeclSpec| $id:ident where $ds;* $[$wds?]?) =>
   `($[$doc?:docComment]? @[$attrs,*] def $id : $ty where
-      name := $(quote id.getId) $[$ds]* $[$wds?]?)
+      name := $(quote id.getId); $ds;* $[$wds?]?)
 | `(targetDeclSpec| $id:ident $[: $ty?]? := $defn $[$wds?]?) =>
   `($[$doc?:docComment]? @[$attrs,*] def $id : $(ty?.getD ty) := $defn $[$wds?]?)
 | `(targetDeclSpec| $id:ident { $[$fs $[,]?]* } $[$wds?]?) => do
-  let defn ← `({ name := $(quote id.getId), $[$fs]* })
+  let defn ← `({ name := $(quote id.getId), $fs,* })
   `($[$doc?:docComment]? @[$attrs,*] def $id : $ty := $defn $[$wds?]?)
 | stx => Macro.throwErrorAt stx "ill-formed target declaration"