trio_example.py

#!/usr/bin/env python
from pathlib import Path

import trio # type: ignore
import time
import sys

from lean_client.trio_server import TrioLeanServer

async def main(path):
    lines = Path(path).read_text().split('\n')

    async with trio.open_nursery() as nursery:
        server = TrioLeanServer(nursery, debug=False)
        await server.start()
        await server.full_sync(path)
        time.sleep(60)

        for i, line in enumerate(lines):
            before = await server.state(path, i+1, 0)
            after = await server.state(path, i+1, len(line))
            if before or after:
                print(f'Line {i+1}: {line}')
                #print(f'State before:\n{before}\n')
                #print(f'State after:\n{after}\n')
            else:
                print(f'Line {i+1}: <skipped>')
        nursery.cancel_scope.cancel()

if __name__ == '__main__':
    path = sys.argv[1]
    trio.run(main, path)