This PR migrates most remaining tests to the new test suite. It also completes the migration of directories like `tests/lean/run`, meaning that PRs trying to add tests to those old directories will now fail.
13 lines
No EOL
1.5 KiB
Text
13 lines
No EOL
1.5 KiB
Text
Content-Length: 242
|
||
|
||
{"jsonrpc":"2.0","method":"textDocument/didChange","params":{"textDocument":{"uri":"file:///test.lean","version":2},"contentChanges":[{"range":{"start":{"line":14,"character":5},"end":{"line":18,"character":12}},"rangeLength":65,"text":""}]}}Content-Length: 241
|
||
|
||
{"jsonrpc":"2.0","method":"textDocument/didChange","params":{"textDocument":{"uri":"file:///test.lean","version":3},"contentChanges":[{"range":{"start":{"line":16,"character":0},"end":{"line":20,"character":0}},"rangeLength":25,"text":""}]}}Content-Length: 241
|
||
|
||
{"jsonrpc":"2.0","method":"textDocument/didChange","params":{"textDocument":{"uri":"file:///test.lean","version":4},"contentChanges":[{"range":{"start":{"line":16,"character":7},"end":{"line":16,"character":13}},"rangeLength":6,"text":""}]}}Content-Length: 242
|
||
|
||
{"jsonrpc":"2.0","method":"textDocument/didChange","params":{"textDocument":{"uri":"file:///test.lean","version":5},"contentChanges":[{"range":{"start":{"line":16,"character":7},"end":{"line":16,"character":7}},"rangeLength":0,"text":"\\"}]}}Content-Length: 241
|
||
|
||
{"jsonrpc":"2.0","method":"textDocument/didChange","params":{"textDocument":{"uri":"file:///test.lean","version":6},"contentChanges":[{"range":{"start":{"line":16,"character":8},"end":{"line":16,"character":8}},"rangeLength":0,"text":"a"}]}}Content-Length: 242
|
||
|
||
{"jsonrpc":"2.0","method":"textDocument/didChange","params":{"textDocument":{"uri":"file:///test.lean","version":7},"contentChanges":[{"range":{"start":{"line":16,"character":7},"end":{"line":16,"character":9}},"rangeLength":2,"text":"α"}]}} |