max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: endPos missing at trace messages

Browse source
This commit is contained in:
Leonardo de Moura 2022-02-28 10:55:07 -08:00
parent b7d2239ca4
commit d89fa9d4c3
2 changed files with 10 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/Lean/Elab/Command.lean
View file

@ -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

5
src/Lean/Elab/Exception.lean
View file

@ -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