diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index a8c438b9dd..1f960cd7da 100644 --- a/src/Lean/Elab/Command.lean +++ b/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 diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean index d648d89f0e..cebd5772c6 100644 --- a/src/Lean/Elab/Frontend.lean +++ b/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 diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean index cea14928a4..103c4f81aa 100644 --- a/src/Lean/Server/Snapshots.lean +++ b/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 diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean index 27fa4d21fb..decd0578cd 100644 --- a/src/Lean/Syntax.lean +++ b/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`. diff --git a/tests/lean/precissues.lean.expected.out b/tests/lean/precissues.lean.expected.out index 6ad63029a9..56b7e6d7ff 100644 --- a/tests/lean/precissues.lean.expected.out +++ b/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 = diff --git a/tests/lean/tokenErrors.lean.expected.out b/tests/lean/tokenErrors.lean.expected.out index 567df327cc..027a00858f 100644 --- a/tests/lean/tokenErrors.lean.expected.out +++ b/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 diff --git a/tests/lean/weirdmacro.lean.expected.out b/tests/lean/weirdmacro.lean.expected.out index d9a1728085..ab28885346 100644 --- a/tests/lean/weirdmacro.lean.expected.out +++ b/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'