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

feat(library/init/lean/syntax): add Syntax.getTailInfo

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-05 16:21:51 -07:00
parent 9d5b0fd309
commit 113ab4824f
1 changed files with 11 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
library/init/lean/syntax.lean
View file

@ -122,7 +122,7 @@ private def updateInfo : SourceInfo → String.Pos → SourceInfo
| {leading := {str := s, startPos := _, stopPos := _}, pos := pos, trailing := trailing} last :=
{leading := {str := s, startPos := last, stopPos := pos}, pos := pos, trailing := trailing}
/- Remark: the State `String.Pos` is the `SourceInfo.trailing.endPos` of the previous token,
/- Remark: the State `String.Pos` is the `SourceInfo.trailing.stopPos` of the previous token,
or the beginning of the String. -/
@[inline]
private def updateLeadingAux : Syntax → State String.Pos (Option Syntax)
@ -166,14 +166,20 @@ partial def updateTrailing (trailing : Substring) : Syntax → Syntax
/-- Retrieve the left-most leaf's info in the Syntax tree. -/
partial def getHeadInfo : Syntax → Option SourceInfo
| (atom info _) := info
| (ident info _ _ _ _ ) := info
| (node _ args _) := args.find getHeadInfo
| _ := none
| missing := none
| (atom info _) := info
| (ident info _ _ _ _) := info
| (node _ args _) := args.find getHeadInfo
def getPos (stx : Syntax) : Option String.Pos :=
SourceInfo.pos <$> stx.getHeadInfo
partial def getTailInfo : Syntax → Option SourceInfo
| missing := none
| (atom info _) := info
| (ident info _ _ _ _) := info
| (node _ args _) := args.findRev getTailInfo
private def reprintLeaf : Option SourceInfo → String → String
| none val := val
| (some info) val := info.leading.toString ++ val ++ info.trailing.toString