diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean index a17cf54619..71e39b7912 100644 --- a/src/Lean/Parser/Module.lean +++ b/src/Lean/Parser/Module.lean @@ -84,12 +84,14 @@ partial def parseCommand (env : Environment) (inputCtx : InputContext) : ModuleP let stx := s.stxStack.back; (stx, { 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; if recovering then - parseCommand { pos := consumeInput c s.pos, recovering := true } messages + parseCommand { pos := pos, recovering := true } messages else let msg := mkErrorMessage c s.pos (toString errorMsg); let messages := messages.add msg; - parseCommand { pos := consumeInput c s.pos, recovering := true } messages + parseCommand { pos := pos, recovering := true } messages private partial def testModuleParserAux (env : Environment) (inputCtx : InputContext) (displayStx : Bool) : ModuleParserState → MessageLog → IO Bool | s, messages => diff --git a/tests/lean/exitAfterParseError.lean b/tests/lean/exitAfterParseError.lean new file mode 100644 index 0000000000..8e3bf2e8c4 --- /dev/null +++ b/tests/lean/exitAfterParseError.lean @@ -0,0 +1,7 @@ +new_frontend + +def foo + +#exit + +def bla diff --git a/tests/lean/exitAfterParseError.lean.expected.out b/tests/lean/exitAfterParseError.lean.expected.out new file mode 100644 index 0000000000..8e6c29a13b --- /dev/null +++ b/tests/lean/exitAfterParseError.lean.expected.out @@ -0,0 +1 @@ +exitAfterParseError.lean:5:0: error: expected ':=' or '|' diff --git a/tests/lean/server/edits.lean.expected.out b/tests/lean/server/edits.lean.expected.out index 64c1f42a54..d4961aec43 100644 --- a/tests/lean/server/edits.lean.expected.out +++ b/tests/lean/server/edits.lean.expected.out @@ -36,12 +36,12 @@ Content-Length: 221 {"params":{"version":9,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":14,"character":31},"end":{"line":14,"character":31}},"message":"expected term"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 184 -{"params":{"version":9,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 1209 +{"params":{"version":9,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 882 -{"params":{"version":10,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":16,"character":0},"end":{"line":16,"character":0}},"message":"expected term"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":20,"character":0},"end":{"line":20,"character":0}},"message":"invalid 'end', insufficient scopes"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":22,"character":7},"end":{"line":22,"character":7}},"message":"unknown identifier 'MyNs.u'"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"sorryAx ?m : ?m"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 185 +{"params":{"version":10,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":16,"character":0},"end":{"line":16,"character":0}},"message":"expected term"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 185 {"params":{"version":10,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 740 {"params":{"version":11,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 38 -{"result":null,"jsonrpc":"2.0","id":1} +{"result":null,"jsonrpc":"2.0","id":1}