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

fix: fixes #2006

Browse source
This commit is contained in:
Leonardo de Moura 2023-01-04 08:19:22 -08:00
parent 069f08e3a3
commit 6fea2946c2
3 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -41,7 +41,7 @@ def parseHeader (inputCtx : InputContext) : IO (Syntax × ModuleParserState × M
let p := andthenFn whitespace Module.header.fn
let tokens := Module.updateTokens (getTokenTable dummyEnv)
let s := p.run inputCtx { env := dummyEnv, options := {} } tokens (mkParserState inputCtx.input)
let stx := s.stxStack.back
let stx := if s.stxStack.isEmpty then .missing else s.stxStack.back
match s.errorMsg with
| some errorMsg =>
let msg := mkErrorMessage inputCtx s.pos (toString errorMsg)

1
tests/lean/2006.lean Normal file
View file

@ -0,0 +1 @@
/-

1
tests/lean/2006.lean.expected.out Normal file
View file

@ -0,0 +1 @@
2006.lean:2:0: error: unterminated comment