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

fix tokenFnAux

Browse source
This commit is contained in:
Leonardo de Moura 2020-06-04 09:09:17 -07:00
parent 8dde9715a9
commit fa2e943c27
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Parser/Parser.lean
View file

@ -104,7 +104,7 @@ structure ParserCache :=
def initCacheForInput (input : String) : ParserCache :=
{ tokenCache := { startPos := input.bsize + 1 /- make sure it is not a valid position -/} }
abbrev TokenTable := Trie Unit
abbrev TokenTable := Trie Token
abbrev SyntaxNodeKindSet := PersistentHashMap SyntaxNodeKind Unit
@ -876,8 +876,8 @@ private def tokenFnAux : ParserFn
else if curr == '`' && isIdFirstOrBeginEscape (getNext input i) then
nameLitAux i c s
else
let (_, _) := c.tokens.matchPrefix input i;
identFnAux i input Name.anonymous c s
let (_, tk) := c.tokens.matchPrefix input i;
identFnAux i tk Name.anonymous c s
private def updateCache (startPos : Nat) (s : ParserState) : ParserState :=
match s with
@ -1665,7 +1665,7 @@ private def mergePrecendences (msgPreamble : String) (sym : String) : Option Nat
private def addTokenConfig (tokens : TokenTable) (tk : Token) : Except String TokenTable := do
if tk == "" then throw "invalid empty symbol"
else match tokens.find? tk with
| none => pure $ tokens.insert tk ()
| none => pure $ tokens.insert tk tk
| some _ => pure tokens
def throwUnknownParserCategory {α} (catName : Name) : ExceptT String Id α :=