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

feat: elaborate syntactically incorrect commands

Browse source
This commit is contained in:
Leonardo de Moura 2021-03-31 13:06:33 -07:00
parent ee55ac5508
commit de024274fe
1 changed files with 6 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Lean/Parser/Module.lean
View file

@ -82,9 +82,9 @@ partial def parseCommand (inputCtx : InputContext) (pmctx : ParserModuleContext)
let s := { cache := initCacheForInput c.input, pos := pos : ParserState }
let s := whitespace c s
let s := topLevelCommandParserFn c s
let stx := s.stxStack.back
match s.errorMsg with
| none => (stx, { pos := s.pos }, messages)
| none =>
(s.stxStack.back, { pos := s.pos }, messages)
| some errorMsg =>
-- advance at least one token to prevent infinite loops
let pos := if s.pos == pos then consumeInput c s.pos else s.pos
@ -93,11 +93,10 @@ partial def parseCommand (inputCtx : InputContext) (pmctx : ParserModuleContext)
else
let msg := mkErrorMessage c s.pos (toString errorMsg)
let messages := messages.add msg
-- We should replace the following line with commented one if we want to elaborate commands containing Syntax errors.
-- This is useful for implementing features such as autocompletion.
-- Right now, it is disabled since `match_syntax` fails on "partial" `Syntax` objects.
parse { pos := pos, recovering := true } messages
-- (stx, { pos := pos, recovering := true }, messages)
if s.stxStack.isEmpty then
parse { pos := pos, recovering := true } messages
else
(s.stxStack.back, { pos := pos, recovering := true }, messages)
parse s messages
-- only useful for testing since most Lean files cannot be parsed without elaboration