From c9cbe35916393604e6b5eea704bfc64304c823d9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 20 Nov 2020 15:37:02 -0800
Subject: [PATCH] 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          |  3 ++-
 src/Lean/Delaborator.lean                   |  8 ++++++--
 src/Lean/Elab/Inductive.lean                |  2 +-
 src/Lean/Elab/PreDefinition/Structural.lean | 16 +++++++++-------
 src/Std/Data/PersistentArray.lean           |  3 ++-
 5 files changed, 20 insertions(+), 12 deletions(-)

diff --git a/src/Lean/Data/Lsp/Diagnostics.lean b/src/Lean/Data/Lsp/Diagnostics.lean
index 45e3b29edc..59ab0f34a4 100644
--- a/src/Lean/Data/Lsp/Diagnostics.lean
+++ b/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
diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean
index 9662999dc4..5e12f27580 100644
--- a/src/Lean/Delaborator.lean
+++ b/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
diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index 7eb53ed12b..7454d035eb 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/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)
diff --git a/src/Lean/Elab/PreDefinition/Structural.lean b/src/Lean/Elab/PreDefinition/Structural.lean
index e5320a851c..34f503434b 100644
--- a/src/Lean/Elab/PreDefinition/Structural.lean
+++ b/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
diff --git a/src/Std/Data/PersistentArray.lean b/src/Std/Data/PersistentArray.lean
index 1024cfd48c..ac5bc5769e 100644
--- a/src/Std/Data/PersistentArray.lean
+++ b/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 }