From 77609dcdc724033daf403d05b81494bb588b05fa Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Mon, 10 Mar 2025 11:37:39 -0400
Subject: [PATCH] feat: lake: config field autocomplete in whitespace (#7393)

This PR adds autocompletion support for Lake configuration fields in the
Lean DSL at the indented whitespace after an existing field.
Autocompletion in the absence of any fields is currently still not
supported.

**Breaking change:** The nonstandard braced configuration syntax now
uses a semicolon `;` rather than a comma `,` as a separator. Indentation
can still be used as an alternative to the separator.
---
 src/lake/Lake/DSL/DeclUtil.lean | 36 ++++++++++++++++++++++-----------
 1 file changed, 24 insertions(+), 12 deletions(-)

diff --git a/src/lake/Lake/DSL/DeclUtil.lean b/src/lake/Lake/DSL/DeclUtil.lean
index 6bff854c2f..e5b2c4558c 100644
--- a/src/lake/Lake/DSL/DeclUtil.lean
+++ b/src/lake/Lake/DSL/DeclUtil.lean
@@ -46,7 +46,7 @@ syntax declField :=
 @[inherit_doc declField] abbrev DeclField := TSyntax ``declField
 
 syntax structVal :=
-  "{" manyIndent(group(declField ", "?)) "}"
+  "{" structInstFields(sepByIndentSemicolon(declField)) "}"
 
 syntax declValDo :=
   ppSpace Term.do (Term.whereDecls)?
@@ -55,7 +55,7 @@ syntax declValStruct :=
   ppSpace structVal (Term.whereDecls)?
 
 syntax declValWhere :=
-  " where " sepByIndentSemicolon(declField) (Term.whereDecls)?
+  " where " structInstFields(sepByIndentSemicolon(declField)) (Term.whereDecls)?
 
 syntax simpleDeclSig :=
   ident Term.typeSpec declValSimple
@@ -87,7 +87,7 @@ structure Field where
   ref : Syntax
   val : Term
 
-open Lean Elab Command
+open Lean Syntax Elab Command
 
 def elabConfigDecl
   (tyName : Name)
@@ -95,7 +95,7 @@ def elabConfigDecl
   (doc? : Option DocComment) (attrs : Array AttrInstance)
   (name? : Option Name := none)
 : CommandElabM PUnit := do
-  let mkCmd (bodyRef : Syntax) (nameStx? : Option IdentOrStr) (fs : TSyntaxArray ``declField) wds? := do
+  let mkCmd (whereInfo : SourceInfo) (nameStx? : Option IdentOrStr) (fs : TSyntaxArray ``declField) wds? := do
     let mut m := mkNameMap Field
     let nameId? := nameStx?.map expandIdentOrStrAsIdent
     if let some id := nameId? then
@@ -109,8 +109,12 @@ def elabConfigDecl
         m := m.insert fieldName {ref := id, val}
       else
         logWarningAt id m!"unknown '{.ofConstName tyName}' field '{fieldName}'"
-    let fs ← m.foldM (init := #[]) fun a k {ref, val} => withRef ref do
-      return a.push <| ← `(Term.structInstField| $(← mkIdentFromRef k true):ident := $val)
+    let fs ← m.foldM (init := #[]) fun a k {ref, val} => do
+      let id := mkIdentFrom ref k true
+      -- An unhygienic quotation is used to avoid introducing source info
+      -- which will break field auto-completion.
+      let fieldStx := Unhygienic.run `(Term.structInstField| $id:ident := $val)
+      return a.push fieldStx
     let ty := mkCIdentFrom (← getRef) tyName
     let declId ← id do
       if let some id := nameId? then
@@ -123,14 +127,22 @@ def elabConfigDecl
           mkIdentFromRef name
         else
           Elab.Term.mkFreshIdent (← getRef)
-    let defn ← withRef bodyRef `({$[$fs:structInstField],*})
-    let cmd ← `($[$doc?]? @[$attrs,*] abbrev $declId : $ty := $defn $[$wds?:whereDecls]?)
+    /-
+    Quotation syntax produces synthetic source information.
+    However, field auto-completion requires the trailing position of this token,
+    which can only be obtained from the original source info. Thus, we must
+    construct this token manually to preserve its original source info.
+    -/
+    let whereTk := atom whereInfo "where"
+    let fields := mkNode ``Term.structInstFields #[mkSep fs mkNullNode]
+    let whereStx := mkNode ``whereStructInst #[whereTk, fields, mkOptionalNode wds?]
+    let cmd ← `($[$doc?]? @[$attrs,*] abbrev $declId : $ty $whereStx:whereStructInst)
     withMacroExpansion sig cmd <| elabCommand cmd
   match sig with
   | `(structDeclSig| $nameStx:identOrStr) =>
-    mkCmd (← getRef) nameStx #[] none
+    mkCmd .none nameStx #[] none
   | `(structDeclSig| $[$nameStx?]? where%$tk $fs;* $[$wds?:whereDecls]?) =>
-    mkCmd tk nameStx? fs.getElems wds?
-  | `(structDeclSig| $[$nameStx?]? { $[$fs $[,]?]* }%$tk $[$wds?:whereDecls]?) =>
-    mkCmd tk nameStx? fs wds?
+    mkCmd tk.getHeadInfo nameStx? fs.getElems wds?
+  | `(structDeclSig| $[$nameStx?]? {%$tk $fs;* } $[$wds?:whereDecls]?) =>
+    mkCmd tk.getHeadInfo nameStx? fs wds?
   | stx => throwErrorAt stx "ill-formed configuration syntax"