feat: adjust message range on unexpected token error

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

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

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⟩

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

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