From d89fa9d4c375d14291ee643c3248ce0a550df033 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Feb 2022 10:55:07 -0800 Subject: [PATCH] fix: `endPos` missing at trace messages --- src/Lean/Elab/Command.lean | 11 +++++++---- src/Lean/Elab/Exception.lean | 5 +++-- 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 022c5c6a38..5689fdc3e8 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -109,7 +109,9 @@ instance : AddErrorMessageContext CommandElabM where return (ref, msg) def mkMessageAux (ctx : Context) (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity) : Message := - mkMessageCore ctx.fileName ctx.fileMap msgData severity (ref.getPos?.getD ctx.cmdPos) + let pos := ref.getPos?.getD ctx.cmdPos + let endPos := ref.getTailPos?.getD pos + mkMessageCore ctx.fileName ctx.fileMap msgData severity pos endPos private def mkCoreContext (ctx : Context) (s : State) (heartbeats : Nat) : Core.Context := let scope := s.scopes.head! @@ -197,9 +199,10 @@ builtin_initialize commandElabAttribute : KeyedDeclsAttribute CommandElab ← mk private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceState : TraceState) : MessageLog := traceState.traces.foldl (init := log) fun (log : MessageLog) traceElem => - let ref := replaceRef traceElem.ref ctx.ref; - let pos := ref.getPos?.getD 0; - log.add (mkMessageCore ctx.fileName ctx.fileMap traceElem.msg MessageSeverity.information pos) + let ref := replaceRef traceElem.ref ctx.ref + let pos := ref.getPos?.getD 0 + let endPos := ref.getTailPos?.getD pos + log.add (mkMessageCore ctx.fileName ctx.fileMap traceElem.msg MessageSeverity.information pos endPos) private def addTraceAsMessages : CommandElabM Unit := do let ctx ← read diff --git a/src/Lean/Elab/Exception.lean b/src/Lean/Elab/Exception.lean index f1e49c6829..39f49037cc 100644 --- a/src/Lean/Elab/Exception.lean +++ b/src/Lean/Elab/Exception.lean @@ -59,8 +59,9 @@ def isAbortTacticException (ex : Exception) : Bool := def isAbortExceptionId (id : InternalExceptionId) : Bool := id == abortCommandExceptionId || id == abortTermExceptionId || id == abortTacticExceptionId -def mkMessageCore (fileName : String) (fileMap : FileMap) (msgData : MessageData) (severity : MessageSeverity) (pos : String.Pos) : Message := +def mkMessageCore (fileName : String) (fileMap : FileMap) (data : MessageData) (severity : MessageSeverity) (pos : String.Pos) (endPos : String.Pos) : Message := let pos := fileMap.toPosition pos - { fileName := fileName, pos := pos, data := msgData, severity := severity } + let endPos := fileMap.toPosition endPos + { fileName, pos, endPos, data, severity } end Lean.Elab