Add optional file ID to document state

jupyter-server / jupyter_ydoc

Jupyter document structures for collaborative editing using Yjs/pycrdt

https://jupyter-ydoc.readthedocs.io

BSD 3-Clause "New" or "Revised" License

27 stars 17 forks source link

Add optional file ID to document state #198

Open davidbrochart opened 8 months ago

davidbrochart commented 8 months ago

The document state already has file-related fields, like "dirty" and "path". Adding "file_id" would make it easy to access it anywhere the shared document is available.