refactor: move elaboration error filtering into Elab.Command

Also make it dependent on presence of `missing` instead of parse error,
which means that messages from complete commands that are immediately followed
by parse errors are not filtered out anymore

src/Lean/Elab/Command.lean

@@ -206,7 +206,12 @@ instance : MonadRecDepth CommandElabM where
   getRecDepth      := return (← read).currRecDepth
   getMaxRecDepth   := return (← get).maxRecDepth
 
-@[inline] def withLogging (x : CommandElabM Unit) : CommandElabM Unit :=
+register_builtin_option showPartialSyntaxErrors : Bool := {
+  defValue := false
+  descr    := "show elaboration errors from partial syntax trees (i.e. after parser recovery)"
+}
+
+@[inline] def withLogging (x : CommandElabM Unit) : CommandElabM Unit := do
   try
     x
   catch ex => match ex with
@@ -232,6 +237,7 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
     if checkTraceOption (← getOptions) `Elab.info then
       logTrace `Elab.info m!"{← tree.format}"
     return tree
+  let initMsgs := (← get).messages
   withLogging <| withRef stx <| withInfoTreeContext (mkInfoTree := mkInfoTree) <| withIncRecDepth <| withFreshMacroScope do
     runLinters stx
     match stx with
@@ -255,6 +261,10 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
           | some elabFns => elabCommandUsing s stx elabFns
           | none         => throwError "elaboration function for '{k}' has not been implemented"
     | _ => throwError "unexpected command"
+  -- `stx.hasMissing` should imply `initMsgs.hasErrors`, but the latter should be cheaper to check in general
+  if !showPartialSyntaxErrors.get (← getOptions) && initMsgs.hasErrors && stx.hasMissing then
+    -- discard elaboration errors on parse error
+    modify ({ · with messages := initMsgs})
 
 /-- Adapt a syntax transformation to a regular, command-producing elaborator. -/
 def adaptExpander (exp : Syntax → CommandElabM Syntax) : CommandElab := fun stx => do

src/Lean/Elab/Frontend.lean

@@ -49,11 +49,6 @@ def setParserState (ps : Parser.ModuleParserState) : FrontendM Unit := modify fu
 def setMessages (msgs : MessageLog) : FrontendM Unit := modify fun s => { s with commandState := { s.commandState with messages := msgs } }
 def getInputContext : FrontendM Parser.InputContext := do pure (← read).inputCtx
 
-register_builtin_option showPartialSyntaxErrors : Bool := {
-  defValue := false
-  descr    := "show elaboration errors from partial syntax tree (i.e. after parser recovery)"
-}
-
 def processCommand : FrontendM Bool := do
   updateCmdPos
   let cmdState ← getCommandState
@@ -62,18 +57,15 @@ def processCommand : FrontendM Bool := do
   let scope := cmdState.scopes.head!
   let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
   let pos := ictx.fileMap.toPosition pstate.pos
-  match profileit "parsing" scope.opts fun _ => Parser.parseCommand ictx pmctx pstate {} with
-  | (cmd, ps, parseMessages) =>
+  match profileit "parsing" scope.opts fun _ => Parser.parseCommand ictx pmctx pstate cmdState.messages with
+  | (cmd, ps, messages) =>
     modify fun s => { s with commands := s.commands.push cmd }
     setParserState ps
-    setMessages (cmdState.messages ++ parseMessages)
+    setMessages messages
     if Parser.isEOI cmd || Parser.isExitCommand cmd then
       pure true -- Done
     else
       profileitM IO.Error "elaboration" scope.opts <| elabCommandAtFrontend cmd
-      if parseMessages.hasErrors && !showPartialSyntaxErrors.get scope.opts then
-        -- discard elaboration errors
-        setMessages (cmdState.messages ++ parseMessages)
       pure false
 
 partial def processCommands : FrontendM Unit := do

src/Lean/Server/Snapshots.lean

@@ -6,7 +6,8 @@ Authors: Wojciech Nawrocki
 -/
 import Init.System.IO
 
-import Lean.Elab.Frontend
+import Lean.Elab.Import
+import Lean.Elab.Command
 
 /-! One can think of this module as being a partial reimplementation
 of Lean.Elab.Frontend which also stores a snapshot of the world after
@@ -90,13 +91,13 @@ def compileNextCmd (contents : String) (snap : Snapshot) : IO (Sum Snapshot Mess
   let cmdState := snap.cmdState
   let scope := cmdState.scopes.head!
   let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
-  let (cmdStx, cmdParserState, parserMessages) :=
-    Parser.parseCommand inputCtx pmctx snap.mpState {}
+  let (cmdStx, cmdParserState, msgLog) :=
+    Parser.parseCommand inputCtx pmctx snap.mpState snap.msgLog
   let cmdPos := cmdStx.getPos?.get!
   if Parser.isEOI cmdStx || Parser.isExitCommand cmdStx then
-    Sum.inr (snap.msgLog ++ parserMessages)
+    Sum.inr msgLog
   else
-    let cmdStateRef ← IO.mkRef { snap.cmdState with messages := snap.msgLog ++ parserMessages }
+    let cmdStateRef ← IO.mkRef { snap.cmdState with messages := msgLog }
     let cmdCtx : Elab.Command.Context := {
         cmdPos   := snap.endPos
         fileName := inputCtx.fileName
@@ -106,10 +107,7 @@ def compileNextCmd (contents : String) (snap : Snapshot) : IO (Sum Snapshot Mess
       Elab.Command.catchExceptions
         (Elab.Command.elabCommand cmdStx)
         cmdCtx cmdStateRef
-    let mut postCmdState ← cmdStateRef.get
-    if parserMessages.hasErrors && !Frontend.showPartialSyntaxErrors.get scope.opts then
-      -- discard elaboration errors
-      postCmdState := { postCmdState with messages := snap.msgLog ++ parserMessages }
+    let postCmdState ← cmdStateRef.get
     let postCmdSnap : Snapshot := {
         beginPos := cmdPos
         stx := cmdStx

src/Lean/Syntax.lean

@@ -229,6 +229,12 @@ where
     -- guaranteed.
     | _                                => s!" {val} "
 
+def hasMissing (stx : Syntax) : Bool := do
+  for stx in stx.topDown do
+    if stx.isMissing then
+      return true
+  return false
+
 /--
 Represents a cursor into a syntax tree that can be read, written, and advanced down/up/left/right.
 Indices are allowed to be out-of-bound, in which case `cur` is `Syntax.missing`.

tests/lean/precissues.lean.expected.out

@@ -5,7 +5,9 @@ f 1 fun (x : Nat) => x : Nat
 f 1 fun (x : Nat) => x : Nat
 id : ?m → ?m
 precissues.lean:15:10: error: expected command
+id : ?m → ?m
 precissues.lean:17:10: error: expected command
+1 : Nat
 id ((fun (this : True) => this) True.intro) : True
 0 = (fun (this : Nat) => this) 1 : Prop
 0 =

tests/lean/tokenErrors.lean.expected.out

@@ -5,3 +5,4 @@ tokenErrors.lean:4:11: error: unterminated identifier escape
 tokenErrors.lean:6:0: error: unterminated comment
 tokenErrors.lean:7:0: error: unterminated comment
 tokenErrors.lean:7:1: error: unterminated comment
+tokenErrors.lean:7:0-7:1: error: unexpected command

tests/lean/weirdmacro.lean.expected.out

@@ -1,3 +1,4 @@
 weirdmacro.lean:1:6: error: expected no space before ':' or string literal
 weirdmacro.lean:1:30-1:32: error: elaboration function for 'antiquot' has not been implemented
 weirdmacro.lean:1:32: error: expected command
+weirdmacro.lean:3:7-3:11: error: unknown identifier 'term'