fix: adjust code to optional , at structure instances

@Kha I implemented the optional `,` at structure instances.
You have suggested it a few weeks/months ago. F# also implements this
feature. I got back to it while write documentation for Lean.
It looks quite nice when we are packing many functions into a structure.

BTW, F# also has optional separators for list literals :)
This is a much simpler change for us since `[...]` is defined using
the `syntax/macro_rules` commands, but I didn't find optional ','
would very useful since our list literals are usually in a single
line.

src/Lean/Data/Lsp/Diagnostics.lean

@@ -137,7 +137,8 @@ def msgToDiagnostic (text : FileMap) (m : Message) : IO Diagnostic := do
     | MessageSeverity.error       => DiagnosticSeverity.error
   let source := "Lean 4 server"
   let message ← m.data.toString
-  pure { range := range,
+  pure {
+    range := range,
     severity? := severity,
     source? := source,
     message := message

src/Lean/Delaborator.lean

@@ -657,9 +657,13 @@ def delabStructureInstance : Delab := whenPPOption getPPStructureInstances do
     -- `ty` is not actually part of `e`, but since `e` must be an application or constant, we know that
     -- index 2 is unused.
     let stxTy ← descend ty 2 delab
-    `({ $fields:structInstField* : $stxTy })
+    return Syntax.node `Lean.Parser.Term.structInst #[
+      mkAtom "{", mkNullNode, mkNullNode fields, mkNullNode,
+      mkNullNode #[ mkAtom ":", stxTy ],
+      mkAtom "}"
+    ]
   else
-    `({ $fields:structInstField* })
+    return Syntax.node `Lean.Parser.Term.structInst #[ mkAtom "{", mkNullNode, mkNullNode fields, mkNullNode, mkNullNode, mkAtom "}"]
 
 @[builtinDelab app.Prod.mk]
 def delabTuple : Delab := whenPPOption getPPNotation do

src/Lean/Elab/Inductive.lean

@@ -59,7 +59,7 @@ structure InductiveView :=
 
 instance : Inhabited InductiveView :=
   ⟨{ ref := arbitrary _, modifiers := {}, shortDeclName := arbitrary _, declName := arbitrary _,
-   levelNames := [], binders := arbitrary _, type? := none, ctors := #[] }⟩
+     levelNames := [], binders := arbitrary _, type? := none, ctors := #[] }⟩
 
 structure ElabHeaderResult :=
   (view       : InductiveView)

src/Lean/Elab/PreDefinition/Structural.lean

@@ -137,13 +137,15 @@ private partial def findRecArg {α} (numFixed : Nat) (xs : Array Expr) (k : RecA
                 let indicesPos := indIndices.map fun index => match ys.indexOf? index with | some i => i.val | none => unreachable!
                 orelse'
                   (mapError
-                    (k { fixedParams := fixedParams, ys := ys, pos := i - fixedParams.size,
-                       indicesPos  := indicesPos,
-                       indName     := indInfo.name,
-                       indLevels   := us,
-                       indParams   := indParams,
-                       indIndices  := indIndices,
-                       reflexive := indInfo.isReflexive })
+                    (k { fixedParams := fixedParams
+                         ys          := ys
+                         pos         := i - fixedParams.size
+                         indicesPos  := indicesPos
+                         indName     := indInfo.name
+                         indLevels   := us
+                         indParams   := indParams
+                         indIndices  := indIndices
+                         reflexive := indInfo.isReflexive })
                     (fun msg => m!"argument #{i+1} was not used for structural recursion{indentD msg}"))
                   (loop (i+1))
     else

src/Std/Data/PersistentArray.lean

@@ -336,7 +336,8 @@ structure Stats :=
 partial def collectStats : PersistentArrayNode α → Stats → Nat → Stats
   | node cs, s, d =>
     cs.foldl (fun s c => collectStats c s (d+1))
-      { s with numNodes := s.numNodes + 1,
+      { s with
+        numNodes := s.numNodes + 1,
         depth    := Nat.max d s.depth }
   | leaf vs, s, d => { s with numNodes := s.numNodes + 1, depth := Nat.max d s.depth }