From e580c903e6b35a76dfc6dcacfe0080e7eefb4422 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 4 Aug 2023 12:48:04 +0200 Subject: [PATCH] feat: adjust message range on unexpected token error --- src/Lean/Message.lean | 14 ++++---- src/Lean/Parser/Module.lean | 18 +++++++--- src/Lean/Widget/InteractiveDiagnostic.lean | 6 ++-- tests/lean/1971.lean | 41 ++++++++++++++++++++++ tests/lean/1971.lean.expected.out | 5 +++ 5 files changed, 69 insertions(+), 15 deletions(-) create mode 100644 tests/lean/1971.lean create mode 100644 tests/lean/1971.lean.expected.out diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 0c9ae5a452..2f6aa8286d 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -208,13 +208,15 @@ end MessageData /-- A `Message` is a richly formatted piece of information emitted by Lean. They are rendered by client editors in the infoview and in diagnostic windows. -/ structure Message where - fileName : String - pos : Position - endPos : Option Position := none - severity : MessageSeverity := MessageSeverity.error - caption : String := "" + fileName : String + pos : Position + endPos : Option Position := none + /-- If `true`, report range as given; see `msgToInteractiveDiagnostic`. -/ + keepFullRange : Bool := false + severity : MessageSeverity := MessageSeverity.error + caption : String := "" /-- The content of the message. -/ - data : MessageData + data : MessageData deriving Inhabited namespace Message diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean index ff3c58482e..5d1ad14929 100644 --- a/src/Lean/Parser/Module.lean +++ b/src/Lean/Parser/Module.lean @@ -32,9 +32,17 @@ structure ModuleParserState where recovering : Bool := false deriving Inhabited -private def mkErrorMessage (c : InputContext) (pos : String.Pos) (errorMsg : String) : Message := - let pos := c.fileMap.toPosition pos - { fileName := c.fileName, pos := pos, data := errorMsg } +private def mkErrorMessage (c : InputContext) (s : ParserState) (e : Parser.Error) : Message := Id.run do + let mut pos := c.fileMap.toPosition s.pos + if e.stopPos?.isSome then + if let .original (trailing := trailing) .. := s.stxStack.back.getTailInfo then + if trailing.stopPos == s.pos then + pos := c.fileMap.toPosition trailing.startPos + { fileName := c.fileName + pos + endPos := c.fileMap.toPosition <$> e.stopPos? + keepFullRange := true + data := toString e } def parseHeader (inputCtx : InputContext) : IO (Syntax × ModuleParserState × MessageLog) := do let dummyEnv ← mkEmptyEnvironment @@ -44,7 +52,7 @@ def parseHeader (inputCtx : InputContext) : IO (Syntax × ModuleParserState × M let stx := if s.stxStack.isEmpty then .missing else s.stxStack.back match s.errorMsg with | some errorMsg => - let msg := mkErrorMessage inputCtx s.pos (toString errorMsg) + let msg := mkErrorMessage inputCtx s errorMsg pure (stx, { pos := s.pos, recovering := true }, { : MessageLog }.add msg) | none => pure (stx, { pos := s.pos }, {}) @@ -96,7 +104,7 @@ partial def parseCommand (inputCtx : InputContext) (pmctx : ParserModuleContext) We claim a syntactically incorrect command containing no token or identifier is irrelevant for intellisense and should be ignored. -/ let ignore := s.stxStack.isEmpty || s.stxStack.back.getPos?.isNone unless recovering && ignore do - messages := messages.add <| mkErrorMessage inputCtx s.pos (toString errorMsg) + messages := messages.add <| mkErrorMessage inputCtx s errorMsg recovering := true if ignore then continue diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean index fb00c239ec..b2cead4ec4 100644 --- a/src/Lean/Widget/InteractiveDiagnostic.lean +++ b/src/Lean/Widget/InteractiveDiagnostic.lean @@ -174,10 +174,8 @@ def msgToInteractiveDiagnostic (text : FileMap) (m : Message) (hasWidgets : Bool | some endPos => /- Truncate messages that are more than one line long. - This is a workaround to avoid big blocks of "red squiggly lines" on VS Code. - TODO: should it be a parameter? - -/ - let endPos := if endPos.line > m.pos.line then { line := m.pos.line + 1, column := 0 } else endPos + This is a workaround to avoid big blocks of "red squiggly lines" on VS Code. -/ + let endPos := if !m.keepFullRange && endPos.line > m.pos.line then { line := m.pos.line + 1, column := 0 } else endPos text.leanPosToLspPos endPos | none => low let range : Range := ⟨low, high⟩ diff --git a/tests/lean/1971.lean b/tests/lean/1971.lean new file mode 100644 index 0000000000..d716b08cb2 --- /dev/null +++ b/tests/lean/1971.lean @@ -0,0 +1,41 @@ +/-! + # More helpful ranges of parser error messages on unexpected tokens + + When the parser hits an unexpected token, it will now include all preceding + whitespace in the error message range as the expected token could be inserted + at any of these places to fix the error. -/ + +/-! + In the following example, we want the parser error to start right after + `exact` as the error belongs to this declaration, not the next one, and + otherwise would be too easy to overlook. -/ + +theorem lem1 : True := by + exact + +theorem lem2 : True := ⟨⟩ + +/-! + Outside of tactics as well it is generally a better idea to place the error + right after the last correct token. -/ + +def f1 + +def f2 := 0 + +/-! + We do not currently special-case linebreaks in this; on a single line, + the shift is usually not very noticeable nor clearly worse than before. -/ + +def f3 := def f4 := 0 + +/-! Test other expected token errors as well -/ + +inductive + +example := 0 + +-- merge of token errors +set_option pp.all + +example := 0 diff --git a/tests/lean/1971.lean.expected.out b/tests/lean/1971.lean.expected.out new file mode 100644 index 0000000000..3f93841972 --- /dev/null +++ b/tests/lean/1971.lean.expected.out @@ -0,0 +1,5 @@ +1971.lean:14:7-16:7: error: expected term +1971.lean:22:6-24:3: error: expected ':=', 'where' or '|' +1971.lean:30:9-30:13: error: expected term +1971.lean:34:9-36:7: error: expected identifier +1971.lean:39:17-41:7: error: expected 'false', 'true', numeral or string literal