chore: address some comments

src/Lean/Data/Json/Basic.lean

@@ -152,7 +152,9 @@ private partial def beq' : Json → Json → Bool
     a == b
   | obj a,  obj b =>
     let _ : BEq Json := ⟨beq'⟩
-    a.all fun field fa =>
+    let szA := a.fold (init := 0) (fun a _ _ => a + 1)
+    let szB := b.fold (init := 0) (fun a _ _ => a + 1)
+    szA == szB && a.all fun field fa =>
       match b.find compare field with
       | none    => false
       | some fb => fa == fb

src/Lean/Data/Lsp/Extra.lean

@@ -48,12 +48,15 @@ structure LeanFileProgressParams where
 
 /-- `$/lean/plainGoal` client->server request.
 
-Returns the goal(s) at the specified position, pretty-printed as a string. -/
+If there is a tactic proof at the specified position, returns the current goals.
+Otherwise returns `null`. -/
 structure PlainGoalParams extends TextDocumentPositionParams
   deriving FromJson, ToJson
 
 structure PlainGoal where
+  /-- The goals as pretty-printed Markdown, or something like "no goals" if accomplished. -/
   rendered : String
+  /-- The pretty-printed goals, empty if all accomplished. -/
   goals : Array String
   deriving FromJson, ToJson
 

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -269,18 +269,16 @@ def delabCore (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (opt
     if !getPPAll opts && getPPAnalyze opts && optionsPerPos.isEmpty then
       withTheReader Core.Context (fun ctx => { ctx with options := opts }) do topDownAnalyze e
     else optionsPerPos
-  let run : Delaborator.DelabM (Syntax × Std.RBMap Pos Elab.Info compare) := do
-    let stx ← Delaborator.delab
-    pure (stx, (← get).infos)
-  catchInternalId Delaborator.delabFailureId
-    (run
+  let (stx, {infos := infos, ..}) ← catchInternalId Delaborator.delabFailureId
+    (Delaborator.delab
       { defaultOptions := opts
         optionsPerPos := optionsPerPos
         currNamespace := currNamespace
         openDecls := openDecls
         subExpr := Delaborator.SubExpr.mkRoot e }
-      |>.run' { : Delaborator.State })
+      |>.run { : Delaborator.State })
     (fun _ => unreachable!)
+  return (stx, infos)
 
 /-- "Delaborate" the given term into surface-level syntax using the default and given subterm-specific options. -/
 def delab (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (optionsPerPos : OptionsPerPos := {}) : MetaM Syntax := do

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -222,7 +222,7 @@ partial def handleDocumentSymbol (p : DocumentSymbolParams)
   let doc ← readDoc
   asTask do
     let ⟨cmdSnaps, e?⟩ ← doc.cmdSnaps.updateFinishedPrefix
-    let mut stxs := cmdSnaps.finishedPrefix.map fun s => s.stx
+    let mut stxs := cmdSnaps.finishedPrefix.map (·.stx)
     match e? with
     | some ElabTaskError.aborted =>
       throw RequestError.fileChanged

src/Lean/Server/Snapshots.lean

@@ -106,21 +106,21 @@ def compileNextCmd (text : FileMap) (snap : Snapshot) : IO Snapshot := do
     Parser.parseCommand inputCtx pmctx snap.mpState snap.msgLog
   let cmdPos := cmdStx.getPos?.get!
   if Parser.isEOI cmdStx || Parser.isExitCommand cmdStx then
-    let endSnap : Snapshot :=
-      { beginPos := cmdPos
-        stx := cmdStx
-        mpState := cmdParserState
-        cmdState := snap.cmdState
-        interactiveDiags := ← newInteractiveDiags msgLog
-      }
+    let endSnap : Snapshot := {
+      beginPos := cmdPos
+      stx := cmdStx
+      mpState := cmdParserState
+      cmdState := snap.cmdState
+      interactiveDiags := ← newInteractiveDiags msgLog
+    }
     endSnap
   else
     let cmdStateRef ← IO.mkRef { snap.cmdState with messages := msgLog }
-    let cmdCtx : Elab.Command.Context :=
-      { cmdPos   := snap.endPos
-        fileName := inputCtx.fileName
-        fileMap  := inputCtx.fileMap
-      }
+    let cmdCtx : Elab.Command.Context := {
+      cmdPos   := snap.endPos
+      fileName := inputCtx.fileName
+      fileMap  := inputCtx.fileMap
+    }
     let (output, _) ← IO.FS.withIsolatedStreams do
       EIO.toIO ioErrorFromEmpty do
         Elab.Command.catchExceptions
@@ -130,20 +130,20 @@ def compileNextCmd (text : FileMap) (snap : Snapshot) : IO Snapshot := do
     if !output.isEmpty then
       postCmdState := {
         postCmdState with
-        messages := postCmdState.messages.add
-          { fileName := inputCtx.fileName
-            severity := MessageSeverity.information
-            pos      := inputCtx.fileMap.toPosition snap.endPos
-            data     := output
-          }
-      }
-    let postCmdSnap : Snapshot :=
-      { beginPos := cmdPos
-        stx := cmdStx
-        mpState := cmdParserState
-        cmdState := postCmdState
-        interactiveDiags := ← newInteractiveDiags postCmdState.messages
+        messages := postCmdState.messages.add {
+          fileName := inputCtx.fileName
+          severity := MessageSeverity.information
+          pos      := inputCtx.fileMap.toPosition snap.endPos
+          data     := output
+        }
       }
+    let postCmdSnap : Snapshot := {
+      beginPos := cmdPos
+      stx := cmdStx
+      mpState := cmdParserState
+      cmdState := postCmdState
+      interactiveDiags := ← newInteractiveDiags postCmdState.messages
+    }
     postCmdSnap
 
 where

src/Lean/Widget/InteractiveDiagnostic.lean

@@ -139,10 +139,7 @@ where
   | nCtx, _,         withContext ctx d        => go nCtx ctx d
   | _,    ctx,       withNamingContext nCtx d => go nCtx ctx d
   | nCtx, ctx,       tagged t d               => do
-    -- tagged is *almost* perfect for detecting traces
-    -- expect for the following two other occurrences:
-    -- src/Lean/Elab/Term.lean:454
-    -- src/Lean/Elab/Tactic/Basic.lean:33
+    -- We postfix trace contexts with `_traceCtx` in order to detect them in messages.
     if let Name.str cls "_traceCtx" _ := t then
       let f ← pushEmbed <| EmbedFmt.lazyTrace nCtx ctx cls d
       Format.tag f s!"[{cls}] (trace hidden)"

src/Lean/Widget/TaggedText.lean

@@ -38,33 +38,29 @@ def appendTag (acc : TaggedText α) (t₀ : α) (a₀ : TaggedText α) : TaggedT
   | text ""   => tag t₀ a₀
   | a         => append #[a, tag t₀ a₀]
 
-partial def map (f : α → β) : TaggedText α → TaggedText β :=
-  go
-where go : TaggedText α → TaggedText β
+variable (f : α → β) in
+partial def map : TaggedText α → TaggedText β
   | text s => text s
-  | append as => append (as.map go)
-  | tag t a => tag (f t) (go a)
+  | append as => append (as.map map)
+  | tag t a => tag (f t) (map a)
 
-partial def mapM [Monad m] (f : α → m β) : TaggedText α → m (TaggedText β) :=
-  go
-where go : TaggedText α → m (TaggedText β)
+variable (f : α → m β) in
+partial def mapM [Monad m] : TaggedText α → m (TaggedText β)
   | text s => text s
-  | append as => do append (← as.mapM go)
-  | tag t a => do tag (← f t) (← go a)
+  | append as => do append (← as.mapM mapM)
+  | tag t a => do tag (← f t) (← mapM a)
 
-partial def rewrite (f : α → TaggedText α → TaggedText β) : TaggedText α → TaggedText β :=
-  go
-where go : TaggedText α → TaggedText β
+variable (f : α → TaggedText α → TaggedText β) in
+partial def rewrite : TaggedText α → TaggedText β
   | text s => text s
-  | append as => append (as.map go)
+  | append as => append (as.map rewrite)
   | tag t a => f t a
 
+variable (f : α → TaggedText α → m (TaggedText β)) in
 /-- Like `mapM` but allows rewriting the whole subtree at `tag` nodes. -/
-partial def rewriteM [Monad m] (f : α → TaggedText α → m (TaggedText β)) : TaggedText α → m (TaggedText β) :=
-  go
-where go : TaggedText α → m (TaggedText β)
+partial def rewriteM [Monad m] : TaggedText α → m (TaggedText β)
   | text s => text s
-  | append as => do append (← as.mapM go)
+  | append as => do append (← as.mapM rewriteM)
   | tag t a => f t a
 
 instance [RpcEncoding α β] : RpcEncoding (TaggedText α) (TaggedText β) where