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

feat: use new endPos field

Browse source
This commit is contained in:
Leonardo de Moura 2021-05-17 15:04:24 -07:00
parent eae1f5412b
commit 54745bda71
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Prelude.lean
View file

@ -1784,9 +1784,9 @@ def getPos? (stx : Syntax) (originalOnly := false) : Option String.Pos :=
partial def getTailPos? (stx : Syntax) (originalOnly := false) : Option String.Pos :=
match stx, originalOnly with
| atom (SourceInfo.original (pos := pos) ..) val, _ => some (pos.add val.bsize)
| atom (SourceInfo.original (endPos := pos) ..) .., _ => some pos
| atom (SourceInfo.synthetic (endPos := pos) ..) _, false => some pos
| ident (SourceInfo.original (pos := pos) ..) val .., _ => some (pos.add val.bsize)
| ident (SourceInfo.original (endPos := pos) ..) .., _ => some pos
| ident (SourceInfo.synthetic (endPos := pos) ..) .., false => some pos
| node _ args, _ =>
let rec loop (i : Nat) : Option String.Pos :=