Skip to content

Feature: Add collaborative text editing using Yjs, y-webrtc and y-monaco #91

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
nileshtrivedi wants to merge 5 commits into
base: main
Choose a base branch
from
Draft

Feature: Add collaborative text editing using Yjs, y-webrtc and y-monaco #91

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
29a80f8
Feature: Add collaborative text editing using Yjs, y-webrtc and y-monaco
nileshtrivedi Mar 13, 2026
e145009
symc with upstream
nileshtrivedi Apr 11, 2026
c1c8475
implement yjs signaling server within index.mjs
nileshtrivedi Apr 11, 2026
5680152
restore top-level package.json
nileshtrivedi Apr 11, 2026
1582aa6
sync with upstream
nileshtrivedi Apr 14, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 4 additions & 1 deletion client/package.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,10 @@
"react-split": "^2.0.14",
"react": "^19.2.0",
"tailwindcss": "^4.1.18",
"vscode-ws-jsonrpc": "^3.5.0"
"vscode-ws-jsonrpc": "^3.5.0",
"y-monaco": "^0.1.6",
"y-webrtc": "^10.3.0",
"yjs": "^13.6.30"
},
"devDependencies": {
"@codingame/esbuild-import-meta-url-plugin": "^1.0.3",
Expand Down
279 changes: 195 additions & 84 deletions client/src/App.tsx
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,11 @@ import { useAtom } from 'jotai/react'
import { LeanMonaco, LeanMonacoEditor, LeanMonacoOptions } from 'lean4monaco'
import * as monaco from 'monaco-editor'
import * as path from 'path'
import { useCallback, useEffect, useRef, useState } from 'react'
import { useCallback, useEffect, useRef, useState, useMemo } from 'react'
import Split from 'react-split'
import * as Y from 'yjs'
import { WebrtcProvider } from 'y-webrtc'
import { MonacoBinding } from 'y-monaco'

import LeanLogo from './assets/logo.svg'
import { codeAtom } from './editor/code-atoms'
Expand Down Expand Up @@ -37,6 +40,14 @@ function App() {
const [, setScreenWidth] = useAtom(screenWidthAtom)
const [project] = useAtom(currentProjectAtom)
const [code, setCode] = useAtom(codeAtom)
const ydoc = useMemo(() => new Y.Doc(), [])
const [provider, setProvider] = useState<WebrtcProvider | null>(null)
const [binding, setBinding] = useState<MonacoBinding | null>(null)
const [collabDialogVisible, setCollabDialogVisible] = useState(false)
const [collabRoomName, setCollabRoomName] = useState('')
const [collabDisplayName, setCollabDisplayName] = useState('')
const [isCollaborating, setIsCollaborating] = useState(false)
const [collabError, setCollabError] = useState('')
const [importedCode] = useAtom(importedCodeAtom)

const model = editor?.getModel()
Expand Down Expand Up @@ -66,6 +77,55 @@ function App() {
return () => window.removeEventListener('resize', handleResize)
}, [setScreenWidth])

// clean up ydoc on unmount
useEffect(() => {
return () => ydoc.destroy()
}, [ydoc])

// this effect manages the lifetime of the Yjs document and the provider
useEffect(() => {
// const provider = new WebsocketProvider('wss://demos.yjs.dev/ws', roomname, ydoc)
// See https://github.com/yjs/y-webrtc for options
if (!isCollaborating || !collabRoomName) {
setProvider(null)
return
}

const signalingUrl = (window.location.protocol === 'https:' ? 'wss://' : 'ws://') + window.location.host.replace(':3000', ':8080') + '/yjs-signaling'
console.log('COLLAB: Signaling URL:', signalingUrl);

const provider = new WebrtcProvider(
collabRoomName, // roomname
ydoc,
{
maxConns: 50,
password: undefined,
signaling: [signalingUrl],
filterBcConns: true,
}
)
if (collabDisplayName) {
provider.awareness.setLocalStateField('user', { name: collabDisplayName })
}
setProvider(provider)
return () => {
provider?.destroy()
}
}, [ydoc, isCollaborating, collabRoomName, collabDisplayName])

// this effect manages the lifetime of the editor binding
useEffect(() => {
if (provider == null || editor == null) {
return
}
console.log('reached', provider)
const binding = new MonacoBinding(ydoc.getText(), editor.getModel()!, new Set([editor]), provider?.awareness)
setBinding(binding)
return () => {
binding.destroy()
}
}, [ydoc, provider, editor])

// Update LeanMonaco options when preferences are loaded or change
useEffect(() => {
if (!project) return
Expand Down Expand Up @@ -114,95 +174,95 @@ function App() {
var leanMonacoEditor = new LeanMonacoEditor()

_leanMonaco.setInfoviewElement(infoviewRef.current!)
;(async () => {
await _leanMonaco.start(options)
await leanMonacoEditor.start(
editorRef.current!,
path.join(project.folder, `${project.folder}.lean`),
code ?? '',
)

setEditor(leanMonacoEditor.editor)
setLeanMonaco(_leanMonaco)

// Add a `Paste` option to the context menu on mobile.
// Monaco does not support clipboard pasting as all browsers block it
// due to security reasons. Therefore we use a codeMirror editor overlay
// which features good mobile support (but no Lean support yet)
if (mobile) {
leanMonacoEditor.editor?.addAction({
id: 'myPaste',
label: "Paste: open 'Plain Editor' for editing on mobile",
// keybindings: [monaco.KeyMod.CtrlCmd | monaco.KeyCode.KEY_V],
contextMenuGroupId: '9_cutcopypaste',
run: (_editor) => {
setCodeMirror(true)
},
})
}
; (async () => {
await _leanMonaco.start(options)
await leanMonacoEditor.start(
editorRef.current!,
path.join(project.folder, `${project.folder}.lean`),
code ?? '',
)

setEditor(leanMonacoEditor.editor)
setLeanMonaco(_leanMonaco)

// Add a `Paste` option to the context menu on mobile.
// Monaco does not support clipboard pasting as all browsers block it
// due to security reasons. Therefore we use a codeMirror editor overlay
// which features good mobile support (but no Lean support yet)
if (mobile) {
leanMonacoEditor.editor?.addAction({
id: 'myPaste',
label: "Paste: open 'Plain Editor' for editing on mobile",
// keybindings: [monaco.KeyMod.CtrlCmd | monaco.KeyCode.KEY_V],
contextMenuGroupId: '9_cutcopypaste',
run: (_editor) => {
setCodeMirror(true)
},
})
}

// // TODO: This was an approach to create a new definition provider, but it
// // wasn't that useful. I'll leave it here in connection with the TODO below for
// // reference.
// monaco.languages.registerDefinitionProvider('lean4', {
// provideDefinition(model, position) {
// const word = model.getWordAtPosition(position);
// if (word) {
// console.log(`[Lean4web] Providing definition for: ${word.word}`);
// // Return the location of the definition
// return [
// {
// uri: model.uri,
// range: {startLineNumber: 0, startColumn: word.startColumn, endColumn: word.endColumn, endLineNumber: 0}, // Replace with actual definition range
// },
// ];
// }
// return null;
// },
// });

// // TODO: This was an approach to create a new definition provider, but it
// // wasn't that useful. I'll leave it here in connection with the TODO below for
// // reference.
// monaco.languages.registerDefinitionProvider('lean4', {
// provideDefinition(model, position) {
// const word = model.getWordAtPosition(position);
// if (word) {
// console.log(`[Lean4web] Providing definition for: ${word.word}`);
// // Return the location of the definition
// return [
// {
// uri: model.uri,
// range: {startLineNumber: 0, startColumn: word.startColumn, endColumn: word.endColumn, endLineNumber: 0}, // Replace with actual definition range
// },
// ];
// }
// return null;
// },
// });

// TODO: Implement Go-To-Definition better
// This approach only gives us the file on the server (plus line number) it wants
// to open, is there a better approach?
const editorService = (leanMonacoEditor.editor as any)?._codeEditorService
if (editorService) {
const openEditorBase = editorService.openCodeEditor.bind(editorService)
editorService.openCodeEditor = async (input: any, source: any) => {
const result = await openEditorBase(input, source)
if (result === null) {
// found this out with `console.debug(input)`:
// `resource.path` is the file go-to-def tries to open on the disk
// we try to create a doc-gen link from that. Could not extract the
// (fully-qualified) decalaration name... with that one could
// call `...${path}.html#${declaration}`
let path = input.resource.path
.replace(new RegExp('^.*/(?:lean|\.lake/packages/[^/]+/)'), '')
.replace(new RegExp('\.lean$'), '')

if (
window.confirm(
`Do you want to open the docs?\n\n${path} (line ${input.options.selection.startLineNumber})`,
)
) {
let newTab = window.open(
`https://leanprover-community.github.io/mathlib4_docs/${path}.html`,
'_blank',
)
if (newTab) {
newTab.focus()
// TODO: Implement Go-To-Definition better
// This approach only gives us the file on the server (plus line number) it wants
// to open, is there a better approach?
const editorService = (leanMonacoEditor.editor as any)?._codeEditorService
if (editorService) {
const openEditorBase = editorService.openCodeEditor.bind(editorService)
editorService.openCodeEditor = async (input: any, source: any) => {
const result = await openEditorBase(input, source)
if (result === null) {
// found this out with `console.debug(input)`:
// `resource.path` is the file go-to-def tries to open on the disk
// we try to create a doc-gen link from that. Could not extract the
// (fully-qualified) decalaration name... with that one could
// call `...${path}.html#${declaration}`
let path = input.resource.path
.replace(new RegExp('^.*/(?:lean|\.lake/packages/[^/]+/)'), '')
.replace(new RegExp('\.lean$'), '')

if (
window.confirm(
`Do you want to open the docs?\n\n${path} (line ${input.options.selection.startLineNumber})`,
)
) {
let newTab = window.open(
`https://leanprover-community.github.io/mathlib4_docs/${path}.html`,
'_blank',
)
if (newTab) {
newTab.focus()
}
}
}
return null
// return result // always return the base result
}
return null
// return result // always return the base result
}
}

// Keeping the `code` state up-to-date with the changes in the editor
leanMonacoEditor.editor?.onDidChangeModelContent(() => {
setCode(leanMonacoEditor.editor?.getModel()?.getValue()!)
})
})()
// Keeping the `code` state up-to-date with the changes in the editor
leanMonacoEditor.editor?.onDidChangeModelContent(() => {
setCode(leanMonacoEditor.editor?.getModel()?.getValue()!)
})
})()
return () => {
leanMonacoEditor.dispose()
_leanMonaco.dispose()
Expand Down Expand Up @@ -269,7 +329,58 @@ function App() {
codeMirror={codeMirror}
setCodeMirror={setCodeMirror}
/>
<button
onClick={() => {
if (isCollaborating) {
setIsCollaborating(false)
} else {
setCollabDialogVisible(true)
}
}}
style={{ marginLeft: '10px', height: 'fit-content', alignSelf: 'center', padding: '4px 8px', borderRadius: '4px', cursor: 'pointer' }}
>
{isCollaborating ? `Collaborating as: ${collabRoomName}/${collabDisplayName}` : 'Collaborate: OFF'}
</button>
</nav>
{collabDialogVisible && (
<div style={{ position: 'fixed', zIndex: 9999, inset: 0, backgroundColor: 'rgba(0,0,0,0.5)', display: 'flex', justifyContent: 'center', alignItems: 'center' }}>
<form
style={{ background: 'var(--vscode-editor-background, white)', color: 'var(--vscode-editor-foreground, black)', padding: '20px', borderRadius: '8px', display: 'flex', flexDirection: 'column', gap: '15px', minWidth: '300px', border: '1px solid var(--vscode-dropdown-border, #ccc)' }}
onSubmit={(e) => {
e.preventDefault();
const isValid = /^[a-z0-9]{3,20}$/;
if (!isValid.test(collabRoomName)) {
setCollabError("Room name must be 3-20 lowercase alphanumeric characters.");
return;
}
if (!isValid.test(collabDisplayName)) {
setCollabError("Display name must be 3-20 lowercase alphanumeric characters.");
return;
}
setCollabError("");
if (collabRoomName) {
setIsCollaborating(true);
setCollabDialogVisible(false);
}
}}
>
<h3 style={{ marginTop: 0, marginBottom: 0 }}>Join Collaboration</h3>
{collabError && <div style={{ color: 'red', fontSize: '14px' }}>{collabError}</div>}
<div style={{ display: 'flex', flexDirection: 'column', gap: '5px' }}>
<label>Room Name:</label>
<input required value={collabRoomName} onChange={e => { setCollabRoomName(e.target.value); setCollabError(''); }} style={{ padding: '6px', backgroundColor: 'var(--vscode-input-background, white)', color: 'var(--vscode-input-foreground, black)', border: '1px solid var(--vscode-input-border, #ccc)' }} />
</div>
<div style={{ display: 'flex', flexDirection: 'column', gap: '5px' }}>
<label>Display Name:</label>
<input required value={collabDisplayName} onChange={e => { setCollabDisplayName(e.target.value); setCollabError(''); }} style={{ padding: '6px', backgroundColor: 'var(--vscode-input-background, white)', color: 'var(--vscode-input-foreground, black)', border: '1px solid var(--vscode-input-border, #ccc)' }} />
</div>
<div style={{ display: 'flex', justifyContent: 'flex-end', gap: '10px', marginTop: '5px' }}>
<button type="button" onClick={() => { setCollabDialogVisible(false); setCollabError(''); }} style={{ padding: '6px 12px', cursor: 'pointer' }}>Cancel</button>
<button type="submit" style={{ padding: '6px 12px', cursor: 'pointer' }}>Join</button>
</div>
</form>
</div>
)}
<Split
className={`editor ${dragging ? 'dragging' : ''}`}
gutter={(_index, _direction) => {
Expand Down
20 changes: 20 additions & 0 deletions client/src/css/index.css
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,3 +22,23 @@ body {
font-family: 'JuliaMono';
src: local('JuliaMono'), url('/fonts/JuliaMono-Regular.ttf');
}

.yRemoteSelection {
background-color: rgb(250, 129, 0, .5)
}
.yRemoteSelectionHead {
position: absolute;
border-left: orange solid 2px;
border-top: orange solid 2px;
border-bottom: orange solid 2px;
height: 100%;
box-sizing: border-box;
}
.yRemoteSelectionHead::after {
position: absolute;
content: ' ';
border: 3px solid orange;
border-radius: 4px;
left: -4px;
top: -5px;
}
Loading