{user.name}
{user.isAdmin &&
Admin interface}
diff --git a/src/app/NavbarExtra.tsx b/src/app/NavbarExtra.tsx
new file mode 100644
index 0000000..7f366d7
--- /dev/null
+++ b/src/app/NavbarExtra.tsx
@@ -0,0 +1,38 @@
+'use client'
+
+import React, { createContext, type ReactNode, type RefObject, use, useLayoutEffect, useRef, useState } from 'react'
+
+type Setter = (_: ReactNode) => void
+const NavbarExtraSetCtx = createContext
| null>(null)
+
+export function NavbarExtraProvider({ children }: Readonly<{ children: ReactNode }>) {
+ const ref = useRef(() => {
+ console.warn('useNavbarExtra called before mounted')
+ })
+ return {children}
+}
+
+/** Renders extra contents of the navbar as set by specific pages.
+ * This component and the page that uses {@link SetNavbarExtra}
+ * must share a {@link NavbarExtraProvider} parent */
+export function NavbarExtra() {
+ const [extra, setExtra] = useState(null)
+ const ref = use(NavbarExtraSetCtx)!
+ useLayoutEffect(() => {
+ ref.current = setExtra
+ }, [ref, setExtra])
+ return extra
+}
+
+/** Sets extra contents of the navbar to its children. */
+export function SetNavbarExtra({ children }: Readonly<{ children: ReactNode }>) {
+ const ref = use(NavbarExtraSetCtx)!
+ React.useEffect(() => {
+ ref.current(children)
+ return () => {
+ // eslint-disable-next-line react-hooks/exhaustive-deps
+ ref.current(null)
+ }
+ }, [ref, children])
+ return null
+}
diff --git a/src/app/[userName]/[projectName]/page.tsx b/src/app/[userName]/[projectName]/page.tsx
index 7406b88..31cf050 100644
--- a/src/app/[userName]/[projectName]/page.tsx
+++ b/src/app/[userName]/[projectName]/page.tsx
@@ -1,6 +1,7 @@
import { requireAuth } from '@/lib/server/actions'
import { getDb } from '@/lib/server/db'
import { getEditorSessionManager } from '@/lib/server/editorSessions'
+import { canAccessProject } from '@/lib/server/util'
import z from 'zod'
const zParams = z.object({
@@ -48,8 +49,7 @@ export default async function EditorSession({ params: params_ }: { params: Promi
const project = await db.project.findUnique({
where: { userId_name: { userId: owner.id, name: params.projectName } },
})
- const isOwner = viewer.name === params.userName
- if (!project || (!isOwner && !project.isPublic)) {
+ if (!project || !canAccessProject(viewer, project)) {
return
}
diff --git a/src/app/api/setup-events/route.ts b/src/app/api/setup-events/route.ts
index 6b8c6ea..abc4d70 100644
--- a/src/app/api/setup-events/route.ts
+++ b/src/app/api/setup-events/route.ts
@@ -1,41 +1,29 @@
import { getSeedState } from '@/lib/server/seed'
+import { sseStreamResponse } from '@/lib/server/util'
export async function GET() {
- const encoder = new TextEncoder()
-
+ // eslint-disable-next-line prefer-const
let interval: ReturnType | undefined
- const stream = new ReadableStream({
- start(controller) {
- let cursor = 0
-
- interval = setInterval(() => {
- const st = getSeedState()
- while (cursor < st.events.length) {
- const event = st.events[cursor++]
- controller.enqueue(encoder.encode(`data: ${JSON.stringify(event)}\n\n`))
- if (event.type === 'done' || event.type === 'error') {
- clearInterval(interval)
- controller.close()
- return
- }
- }
- if (!st.inProgress) {
- clearInterval(interval)
- controller.close()
- }
- }, 500)
- },
- cancel() {
- clearInterval(interval)
- },
+ const [response, send, close] = sseStreamResponse(() => {
+ clearInterval(interval)
})
+ let cursor = 0
+ interval = setInterval(() => {
+ const st = getSeedState()
+ while (cursor < st.events.length) {
+ const event = st.events[cursor++]
+ send(event)
+ if (event.type === 'done' || event.type === 'error') {
+ clearInterval(interval)
+ close()
+ return
+ }
+ }
+ if (!st.inProgress) {
+ clearInterval(interval)
+ close()
+ }
+ }, 500)
- return new Response(stream, {
- headers: {
- 'Content-Type': 'text/event-stream',
- 'Cache-Control': 'no-cache',
- Connection: 'keep-alive',
- 'X-Accel-Buffering': 'no',
- },
- })
+ return response
}
diff --git a/src/app/components/AvatarIcon.tsx b/src/app/components/AvatarIcon.tsx
new file mode 100644
index 0000000..b432a3c
--- /dev/null
+++ b/src/app/components/AvatarIcon.tsx
@@ -0,0 +1,14 @@
+import type { User } from '@/lib/server/auth'
+import Image from 'next/image'
+
+export default function AvatarIcon({ user }: { user: Pick }) {
+ return (
+
+ )
+}
diff --git a/src/app/layout.tsx b/src/app/layout.tsx
index 8581614..7e2e6e6 100644
--- a/src/app/layout.tsx
+++ b/src/app/layout.tsx
@@ -9,6 +9,7 @@ import { connection } from 'next/server'
import { Suspense, type ReactNode } from 'react'
import AvatarMenu from './AvatarMenu'
import Breadcrumbs from './Breadcrumbs'
+import { NavbarExtra, NavbarExtraProvider } from './NavbarExtra'
const openSans = Open_Sans({
subsets: ['latin'],
@@ -56,18 +57,21 @@ async function RootLayoutBody({
{/* https://nextjs.org/docs/app/getting-started/server-and-client-components#interleaving-server-and-client-components */}
-
-
- {children}
-
+
+
+
+ {children}
+
+
)
diff --git a/src/lib/server/collabServer.ts b/src/lib/server/collabServer.ts
index e3e4992..c1cfd1b 100644
--- a/src/lib/server/collabServer.ts
+++ b/src/lib/server/collabServer.ts
@@ -18,6 +18,8 @@ export class CollabServerHandle {
readonly uuid = crypto.randomUUID()
/** Directory in which `collab-server` places its files. */
readonly workDir: string = `/tmp/collab-server-${this.uuid}/`
+ /** Path to the `collab-server` UDS file. */
+ readonly socketPath: string = path.join(this.workDir, COLLAB_SOCKET_FILENAME)
constructor(
/** Project that this server manages. */
diff --git a/src/lib/server/editorSessions.ts b/src/lib/server/editorSessions.ts
index bb77132..4bcabd7 100644
--- a/src/lib/server/editorSessions.ts
+++ b/src/lib/server/editorSessions.ts
@@ -1,9 +1,9 @@
-import { User } from '@/lib/server/auth'
+import type { User } from '@/lib/server/auth'
import { CollabServerHandle } from '@/lib/server/collabServer'
import { getWorkspacesDir } from '@/lib/server/config'
import { getDb } from '@/lib/server/db'
import { VscodeServerHandle } from '@/lib/server/vscodeServer'
-import { Project } from '@/prisma/generated/client'
+import type { Project } from '@/prisma/generated/client'
import path from 'node:path'
import { EventEmitter } from 'node:stream'
import 'server-only'
diff --git a/src/lib/server/util.ts b/src/lib/server/util.ts
index ed12445..9d2ae02 100644
--- a/src/lib/server/util.ts
+++ b/src/lib/server/util.ts
@@ -1,5 +1,7 @@
+import type { Project } from '@/prisma/generated/client'
import fs from 'node:fs/promises'
import 'server-only'
+import type { User } from './auth'
export interface ProcessInfo {
pid: number
@@ -61,3 +63,45 @@ export const BWRAP_ARGS =
export function bwrapProjectDir(projectName: string) {
return `/workspace/${projectName}/`
}
+
+export function canAccessProject(user: User, project: Project) {
+ const isOwner = user.id === project.userId
+ return isOwner || project.isPublic
+}
+
+/** Returns `[response, send, close]`.
+ * See https://developer.mozilla.org/en-US/docs/Web/API/Server-sent_events */
+export function sseStreamResponse(onCancel?: () => void): [Response, (msg: object) => void, () => void] {
+ let send: (msg: object) => void = () => {}
+ let close: () => void = () => {}
+ let closed = false
+ const encoder = new TextEncoder()
+ const stream = new ReadableStream({
+ start(controller) {
+ send = msg => {
+ if (closed) return
+ controller.enqueue(encoder.encode(`data: ${JSON.stringify(msg)}\n\n`))
+ }
+ close = () => {
+ if (closed) return
+ closed = true
+ controller.close()
+ }
+ },
+ cancel() {
+ closed = true
+ if (onCancel) onCancel()
+ },
+ })
+
+ const response = new Response(stream, {
+ headers: {
+ 'Content-Type': 'text/event-stream',
+ 'Cache-Control': 'no-cache',
+ Connection: 'keep-alive',
+ 'X-Accel-Buffering': 'no',
+ },
+ })
+
+ return [response, send, close]
+}
diff --git a/src/lib/server/vscodeServer.ts b/src/lib/server/vscodeServer.ts
index d5a2f0b..45eef11 100644
--- a/src/lib/server/vscodeServer.ts
+++ b/src/lib/server/vscodeServer.ts
@@ -15,6 +15,7 @@ import { ChildProcess, exec, spawn } from 'node:child_process'
import fs from 'node:fs/promises'
import { request } from 'node:http'
import path from 'node:path'
+import type Stream from 'node:stream'
import { promisify } from 'node:util'
/** Create a VSCode machine settings file if one doesn't exist. */
@@ -44,6 +45,8 @@ async function ensureMachineSettings(serverDataDir: string): Promise {
// those edits will be lost.
// FIXME: inform users about this risk, and attempt detection in collab-server.
'files.saveConflictResolution': 'overwriteFileOnDisk',
+ // Auto-save on every keystroke interferes with collaborative editing state.
+ 'files.autoSave': 'off',
},
null,
2,
@@ -212,6 +215,7 @@ export class VscodeServerHandle {
'--bind', this.projectDir, sandboxProjectDir,
'--bind', this.collabWorkDir, '/workspace/.collab-server',
'--bind', this.socketDir, '/workspace/.openvscode-server',
+ '--ro-bind-data', '3', '/workspace/.lean-workbench.json',
...overlayArgs,
'--setenv', 'HOME', '/workspace',
'--setenv', 'ELAN_HOME', getElanDir(),
@@ -228,6 +232,8 @@ export class VscodeServerHandle {
path.join(getOpenVscodeServerDir(), 'bin', 'openvscode-server'),
'--socket-path', `/workspace/.openvscode-server/${VSCODE_SOCKET_FILENAME}`,
'--without-connection-token',
+ // Reduce how long the extension host process waits for a web client to reconnect (default 3h).
+ '--reconnection-grace-time', '60',
`--server-base-path=${this.vscodeIframePath}`,
'--server-data-dir', '/workspace/.vscode-remote',
// TODO: make a per-project user-data-dir to support concurrent editing sessions.
@@ -242,6 +248,8 @@ export class VscodeServerHandle {
})
this.proc = proc
+ const workspaceMdataPipe = proc.stdio[3] as Stream.Writable
+
await Promise.race([
// Reject if errors occur before setup is finished.
new Promise((_, reject) => {
@@ -252,9 +260,20 @@ export class VscodeServerHandle {
proc.once('error', err => {
reject(new Error(`${this.description} failed to start: ${String(err)}`))
})
+ workspaceMdataPipe.once('error', err => {
+ reject(new Error(`${this.description} failed to write workspace metadata: ${String(err)}`))
+ })
}),
// Wait for the server to start listening and for Nginx to be ready.
(async () => {
+ workspaceMdataPipe.end(
+ JSON.stringify({
+ viewer: {
+ name: this.viewer.name,
+ image: this.viewer.image,
+ },
+ }),
+ )
await this.writeNginxUserRoute()
this.disposables.defer(async () => {
await fs.rm(this.nginxUserRoutePath, { force: true })
diff --git a/vscode-workbench/.vscode-test.mjs b/vscode-workbench/.vscode-test.mjs
index 6a36b3f..099761c 100644
--- a/vscode-workbench/.vscode-test.mjs
+++ b/vscode-workbench/.vscode-test.mjs
@@ -2,4 +2,7 @@ import { defineConfig } from '@vscode/test-cli'
export default defineConfig({
files: 'out/test/**/*.test.js',
+ // Stable VS Code gates proposed APIs behind this flag:
+ // `enabledApiProposals` in package.json is ignored without it.
+ launchArgs: ['--enable-proposed-api', 'leanprover.workbench'],
})
diff --git a/vscode-workbench/.vscodeignore b/vscode-workbench/.vscodeignore
index 9f748ab..9413a44 100644
--- a/vscode-workbench/.vscodeignore
+++ b/vscode-workbench/.vscodeignore
@@ -5,4 +5,5 @@
!dist/extension.js
!package.json
-!LICENSE
\ No newline at end of file
+!LICENSE
+!media
\ No newline at end of file
diff --git a/vscode-workbench/esbuild.mjs b/vscode-workbench/esbuild.mjs
index c8c48e1..d575969 100644
--- a/vscode-workbench/esbuild.mjs
+++ b/vscode-workbench/esbuild.mjs
@@ -1,18 +1,23 @@
import esbuild from 'esbuild'
+import { glob } from 'node:fs/promises'
const isProd = process.argv.includes('--production')
const watch = process.argv.includes('--watch')
+const tests = process.argv.includes('--tests')
+
+const testFiles = async () => Array.fromAsync(glob('test/**/*.test.ts'))
const ctx = await esbuild.context({
- entryPoints: ['src/extension.ts'],
bundle: true,
format: 'cjs',
- outfile: 'dist/extension.js',
external: ['vscode'],
- minify: isProd,
sourcemap: !isProd,
platform: 'node',
target: 'node22',
+ define: { 'import.meta.url': '__filename' },
+ ...(tests
+ ? { entryPoints: await testFiles(), outdir: 'out/test' }
+ : { entryPoints: ['src/extension.ts'], outfile: 'dist/extension.js', minify: isProd }),
})
if (watch) {
diff --git a/vscode-workbench/media/logo.svg b/vscode-workbench/media/logo.svg
new file mode 100644
index 0000000..40c20dc
--- /dev/null
+++ b/vscode-workbench/media/logo.svg
@@ -0,0 +1,3 @@
+
diff --git a/vscode-workbench/package.json b/vscode-workbench/package.json
index 48e8382..0a4fda2 100644
--- a/vscode-workbench/package.json
+++ b/vscode-workbench/package.json
@@ -6,7 +6,7 @@
"private": true,
"publisher": "leanprover",
"engines": {
- "vscode": "^1.109.0"
+ "vscode": "1.109.5"
},
"categories": [
"Other"
@@ -18,19 +18,43 @@
"activationEvents": [
"onStartupFinished"
],
+ "enabledApiProposals": [
+ "textDocumentChangeReason",
+ "extensionsAny"
+ ],
+ "contributes": {
+ "viewsContainers": {
+ "activitybar": [
+ {
+ "id": "leanprover-workbench-view-container",
+ "title": "Lean Workbench",
+ "icon": "media/logo.svg"
+ }
+ ]
+ },
+ "views": {
+ "leanprover-workbench-view-container": [
+ {
+ "id": "leanprover-workbench-view",
+ "name": "",
+ "icon": ""
+ }
+ ]
+ }
+ },
"main": "./dist/extension.js",
"scripts": {
"watch": "concurrently --names esbuild,tsc 'npm run watch:esbuild' 'npm run watch:tsc'",
"watch:esbuild": "node esbuild.mjs --watch",
- "watch:tsc": "tsc --noEmit --watch --preserveWatchOutput",
- "tsc": "tsc --noEmit",
- "build": "tsc --noEmit && node esbuild.mjs --production",
+ "watch:tsc": "tsc --watch --preserveWatchOutput",
+ "tsc": "tsc",
+ "build": "tsc && node esbuild.mjs --production",
"vscode:prepublish": "npm run build",
- "test": "tsc && vscode-test"
+ "test": "tsc && node esbuild.mjs --tests && vscode-test"
},
"devDependencies": {
"@types/mocha": "^10.0",
- "@types/vscode": "^1.109",
+ "@types/vscode": "~1.109",
"@types/ws": "^8.18.1",
"@vscode/test-cli": "^0.0.12",
"@vscode/test-electron": "^2.5",
@@ -38,6 +62,7 @@
},
"dependencies": {
"@hocuspocus/provider": "^4.0",
- "ws": "^8.20.0"
+ "ws": "^8.20",
+ "zod": "^4.4"
}
}
diff --git a/vscode-workbench/src/collabServer.ts b/vscode-workbench/src/collabServer.ts
new file mode 100644
index 0000000..77abb9e
--- /dev/null
+++ b/vscode-workbench/src/collabServer.ts
@@ -0,0 +1,101 @@
+import { HocuspocusProvider, HocuspocusProviderWebsocket } from '@hocuspocus/provider'
+import vs from 'vscode'
+import WebSocket from 'ws'
+import type { Awareness } from 'y-protocols/awareness'
+import {
+ AWARENESS_CURSOR_COLORS,
+ AWARENESS_DOC_NAME,
+ AWARENESS_USER_KEY,
+ AwarenessUser,
+ BWRAP_COLLAB_SOCK_PATH,
+ waitForPath,
+ WorkspaceMetadata,
+} from './util'
+
+export class CollabServerConnection implements vs.Disposable {
+ constructor(
+ readonly collabSock: HocuspocusProviderWebsocket,
+ private readonly awarenessProvider: HocuspocusProvider,
+ ) {}
+
+ dispose() {
+ this.awarenessProvider.destroy()
+ this.collabSock.destroy()
+ }
+
+ get awareness(): Awareness {
+ return this.awarenessProvider.awareness!
+ }
+}
+
+export async function connectToCollabServer(
+ log: vs.LogOutputChannel,
+ mdata: WorkspaceMetadata,
+): Promise {
+ const showErrorModal = () => {
+ const action = 'Reload window'
+ void vs.window
+ .showErrorMessage(
+ 'Collaboration server is not available - Lean Workbench will not function correctly.',
+ { modal: true },
+ action,
+ )
+ .then(async s => {
+ if (s === action) {
+ await vs.commands.executeCommand('workbench.action.reloadWindow')
+ }
+ })
+ }
+
+ log.debug('Waiting for collab-server socket..')
+ if (!(await waitForPath(BWRAP_COLLAB_SOCK_PATH, 5_000))) {
+ showErrorModal()
+ return undefined
+ }
+
+ const collabSock = new HocuspocusProviderWebsocket({
+ url: `ws+unix:${BWRAP_COLLAB_SOCK_PATH}:/`,
+ // Must use the `ws` package for https://github.com/websockets/ws/blob/master/doc/ws.md#ipc-connections.
+ WebSocketPolyfill: WebSocket,
+ })
+ log.debug('Opened collab-server socket')
+
+ const awarenessProvider = new HocuspocusProvider({
+ websocketProvider: collabSock,
+ name: AWARENESS_DOC_NAME,
+ })
+ awarenessProvider.attach()
+ // Wait so we can see other clients' colors before picking ours.
+ if (!awarenessProvider.isSynced) {
+ const success = await new Promise(resolve => {
+ awarenessProvider.on('synced', () => resolve(true))
+ setTimeout(() => resolve(false), 5_000)
+ })
+ if (!success) {
+ showErrorModal()
+ return undefined
+ }
+ }
+
+ // Pick the color least used by other clients. Ties are broken by list order.
+ const awareness = awarenessProvider.awareness!
+ const counts = new Map(AWARENESS_CURSOR_COLORS.map(c => [c, 0]))
+ for (const [clientId, state] of awareness.getStates()) {
+ if (clientId === awareness.clientID) continue
+ const user = state[AWARENESS_USER_KEY] as AwarenessUser | undefined
+ if (!user) continue
+ counts.set(user.color, (counts.get(user.color) ?? 0) + 1)
+ }
+ const color = AWARENESS_CURSOR_COLORS.reduce(
+ (acc, c) => (counts.get(acc)! <= counts.get(c)! ? acc : c),
+ AWARENESS_CURSOR_COLORS[0],
+ )
+
+ awarenessProvider.setAwarenessField(AWARENESS_USER_KEY, {
+ name: mdata.viewer.name,
+ image: mdata.viewer.image,
+ color,
+ } satisfies AwarenessUser)
+
+ return new CollabServerConnection(collabSock, awarenessProvider)
+}
diff --git a/vscode-workbench/src/extension.ts b/vscode-workbench/src/extension.ts
index 5917eae..37588f6 100644
--- a/vscode-workbench/src/extension.ts
+++ b/vscode-workbench/src/extension.ts
@@ -1,99 +1,75 @@
-import { HocuspocusProviderWebsocket } from '@hocuspocus/provider'
import fs from 'node:fs/promises'
import vs from 'vscode'
-import WebSocket from 'ws'
-import { RemoteDocManager } from './remoteDoc'
+import { connectToCollabServer } from './collabServer'
+import { WorkbenchPanelProvider } from './panel'
+import { RemoteSelectionDecorator } from './remoteSelections'
import { YTextBindingManager } from './textBinding'
-import { BWRAP_COLLAB_SERVER_DIR, BWRAP_COLLAB_SOCK_PATH } from './util'
+import { BWRAP_METADATA_PATH, WorkspaceMetadata, zWorkspaceMetadata } from './util'
-/** Ensure we are in the expected Lean Workbench environment.
- * Return `false` if we are not,
- * prompting the user to fix this whenever possible. */
-async function ensureWorkbenchEnv(log: vs.LogOutputChannel): Promise {
+/** Ensure we are in the expected Lean Workbench environment
+ * and return the current workspace configuration.
+ * Otherwise display an error and return `undefined`. */
+async function readWorkspaceMdata(log: vs.LogOutputChannel): Promise {
log.debug(`Workspace file: ${JSON.stringify(vs.workspace.workspaceFile)}`)
log.debug(`Workspace folders: ${JSON.stringify(vs.workspace.workspaceFolders)}`)
+ let mdata: WorkspaceMetadata
try {
- await fs.access(BWRAP_COLLAB_SERVER_DIR)
+ const raw = await fs.readFile(BWRAP_METADATA_PATH, 'utf8')
+ mdata = zWorkspaceMetadata.parse(JSON.parse(raw))
} catch (err) {
log.error(String(err))
void vs.window.showErrorMessage('Could not detect the Lean Workbench - shutting down.')
- return false
+ return undefined
}
- return true
+ return mdata
}
-async function waitForPath(p: string, timeoutMs: number): Promise {
- const deadline = Date.now() + timeoutMs
- while (Date.now() < deadline) {
- try {
- await fs.access(p)
- return true
- } catch {}
- await new Promise(r => setTimeout(r, 200))
- }
- return false
+function syncableDirs(): string[] {
+ return (vs.workspace.workspaceFolders ?? []).filter(f => f.uri.scheme === 'file').map(f => f.uri.fsPath)
}
-async function connectToCollabServer(
- ctx: vs.ExtensionContext,
- log: vs.LogOutputChannel,
-): Promise {
- const mk = () => {
- const collabSock = new HocuspocusProviderWebsocket({
- url: `ws+unix:${BWRAP_COLLAB_SOCK_PATH}:/`,
- // Must use the `ws` package for https://github.com/websockets/ws/blob/master/doc/ws.md#ipc-connections.
- WebSocketPolyfill: WebSocket,
- })
- ctx.subscriptions.push({
- dispose() {
- collabSock.destroy()
- },
- })
- log.debug('Opened collab-server socket')
- return collabSock
- }
+/** Extensions that intercept text input and conflict with collaborative editing. */
+const CONFLICTING_EXTENSIONS = ['vscodevim.vim', 'asvetliakov.vscode-neovim']
- log.debug('Waiting for collab-server socket..')
- if (await waitForPath(BWRAP_COLLAB_SOCK_PATH, 5_000)) return mk()
- const action = 'Reload window'
- void vs.window
- .showErrorMessage(
- 'Collaboration server is not available - Lean Workbench will not function correctly.',
- { modal: true },
- action,
+function checkInstalledExtensions(): void {
+ const conflicting = CONFLICTING_EXTENSIONS.filter(id =>
+ vs.extensions.getExtension(id, true /* include browser extensions */),
+ )
+ if (conflicting.length > 0)
+ void vs.window.showErrorMessage(
+ `The following extension(s) are not currently supported in the Lean Workbench - please disable them: ${conflicting.join(', ')}`,
)
- .then(async s => {
- if (s === action) {
- await vs.commands.executeCommand('workbench.action.reloadWindow')
- }
- })
-
- return undefined
-}
-
-function syncableDirs(): string[] {
- return (vs.workspace.workspaceFolders ?? []).filter(f => f.uri.scheme === 'file').map(f => f.uri.fsPath)
}
export async function activate(ctx: vs.ExtensionContext) {
const log = vs.window.createOutputChannel('Lean 4 - Workbench', { log: true })
- if (!(await ensureWorkbenchEnv(log))) return
+ const mdata = await readWorkspaceMdata(log)
+ if (!mdata) return
- const collabSock = await connectToCollabServer(ctx, log)
- if (!collabSock) return
+ checkInstalledExtensions()
+ ctx.subscriptions.push(vs.extensions.onDidChange(checkInstalledExtensions))
- const docs = new RemoteDocManager(collabSock, log)
+ const collabServer = await connectToCollabServer(log, mdata)
+ if (!collabServer) return
+ ctx.subscriptions.push(collabServer)
// We apply collaborative syncing to open folders (usually just the project folder) only.
// User-specific folders such as /workspace/.vscode-remote are not synced
// (though they would be if someone opens /workspace - TODO better UX).
- const bindings = new YTextBindingManager(docs, syncableDirs(), log)
+ const bindings = new YTextBindingManager(collabServer.collabSock, syncableDirs(), log)
ctx.subscriptions.push(
bindings,
vs.workspace.onDidChangeWorkspaceFolders(() => bindings.updateSyncableDirs(syncableDirs())),
+ // Remote presence indicators
+ new RemoteSelectionDecorator(collabServer.awareness),
)
+
+ // Panel with workbench-specific information
+ const panel = new WorkbenchPanelProvider(collabServer.awareness, mdata, log)
+ ctx.subscriptions.push(panel, vs.window.registerTreeDataProvider('leanprover-workbench-view', panel))
+
log.debug('Extension activated')
}
diff --git a/vscode-workbench/src/panel.ts b/vscode-workbench/src/panel.ts
new file mode 100644
index 0000000..2656066
--- /dev/null
+++ b/vscode-workbench/src/panel.ts
@@ -0,0 +1,133 @@
+import vs from 'vscode'
+import { Awareness } from 'y-protocols/awareness'
+import {
+ AWARENESS_SELECTION_KEY,
+ AWARENESS_USER_KEY,
+ AwarenessSelection,
+ AwarenessUser,
+ equalAwarenessUsers,
+ equalMaps,
+ Logger,
+ logWithPrefix,
+ WorkspaceMetadata,
+} from './util'
+
+type PanelItem = { kind: 'onlineUsersRoot' } | { kind: 'onlineUser'; user: AwarenessUser }
+
+const COMMAND_GOTO_AWARENESS_USER = 'leanprover.workbench.internal.goToAwarenessUser'
+
+// Copied from vscode-lean4
+async function revealEditorSelection(fsPath: string, selection?: vs.Selection) {
+ let editor = vs.window.visibleTextEditors.find(v => v.document.uri.fsPath === fsPath)
+ if (editor === undefined) {
+ editor = await vs.window.showTextDocument(vs.Uri.file(fsPath), {
+ viewColumn: vs.window.activeTextEditor?.viewColumn ?? vs.ViewColumn.One,
+ preserveFocus: false,
+ })
+ }
+ if (selection !== undefined) {
+ editor.revealRange(selection, vs.TextEditorRevealType.InCenterIfOutsideViewport)
+ editor.selection = selection
+ // ensure the text document has the keyboard focus.
+ await vs.window.showTextDocument(editor.document, { viewColumn: editor.viewColumn, preserveFocus: false })
+ }
+}
+
+// https://code.visualstudio.com/api/extension-guides/tree-view
+export class WorkbenchPanelProvider implements vs.TreeDataProvider, vs.Disposable {
+ /** username ↦ client data */
+ private onlineUsers = new Map()
+
+ private readonly onDidChangeTreeDataEmitter = new vs.EventEmitter()
+ readonly onDidChangeTreeData = this.onDidChangeTreeDataEmitter.event
+
+ private readonly disposables: vs.Disposable[] = []
+
+ private readonly log: Logger
+
+ constructor(
+ private readonly awareness: Awareness,
+ private readonly mdata: WorkspaceMetadata,
+ log_: Logger,
+ ) {
+ this.log = logWithPrefix(log_, '[WorkbenchPanelProvider]')
+
+ const onAwarenessChange = () => this.onAwarenessChange()
+ awareness.on('change', onAwarenessChange)
+ this.disposables.push(
+ { dispose: () => awareness.off('change', onAwarenessChange) },
+ vs.commands.registerCommand(COMMAND_GOTO_AWARENESS_USER, async (userName: string) => {
+ let filePath: string | undefined = undefined
+ let sel: vs.Selection | undefined = undefined
+ // One user can have multiple active sessions.
+ // We arbitrarily choose the first remote session with a non-empty selection.
+ for (const [clientId, state] of awareness.getStates()) {
+ if (this.awareness.clientID === clientId) continue
+ const user = state[AWARENESS_USER_KEY] as AwarenessUser | undefined
+ if (!user || user.name !== userName) continue
+ const sels = state[AWARENESS_SELECTION_KEY] as AwarenessSelection | undefined
+ if (!sels) continue
+ filePath = sels.filePath
+ if (0 < sels.selections.length) {
+ const active = sels.selections[0].active
+ const pos = new vs.Position(active.line, active.character)
+ sel = new vs.Selection(pos, pos)
+ break
+ }
+ }
+ if (filePath) await revealEditorSelection(filePath, sel)
+ }),
+ )
+ this.onAwarenessChange()
+ }
+
+ onAwarenessChange() {
+ const newUsers = new Map()
+ for (const [, state] of this.awareness.getStates()) {
+ const user = state[AWARENESS_USER_KEY] as AwarenessUser | undefined
+ // The same user can appear multiple times, e.g. when opening a project tab twice.
+ // FIXME: show with multiplicity?
+ if (user) newUsers.set(user.name, user)
+ }
+ if (equalMaps(this.onlineUsers, newUsers, equalAwarenessUsers)) return
+ this.log.debug(`users changed: ${JSON.stringify([...newUsers])}`)
+ this.onlineUsers = newUsers
+ this.onDidChangeTreeDataEmitter.fire()
+ }
+
+ getTreeItem(item: PanelItem): vs.TreeItem {
+ switch (item.kind) {
+ case 'onlineUsersRoot':
+ return new vs.TreeItem('Online users', vs.TreeItemCollapsibleState.Expanded)
+ case 'onlineUser': {
+ let displayName = item.user.name
+ if (item.user.name === this.mdata.viewer.name) displayName += ' (You)'
+ const ti = new vs.TreeItem(displayName, vs.TreeItemCollapsibleState.None)
+ let iconUri: vs.Uri | undefined = undefined
+ try {
+ if (item.user.image) iconUri = vs.Uri.parse(item.user.image, true)
+ } catch {}
+ ti.iconPath = iconUri ? iconUri : new vs.ThemeIcon('account')
+ ti.command = { command: COMMAND_GOTO_AWARENESS_USER, title: 'Jump to cursor', arguments: [item.user.name] }
+ return ti
+ }
+ }
+ }
+
+ getChildren(item?: PanelItem): PanelItem[] {
+ if (!item) return [{ kind: 'onlineUsersRoot' }]
+ if (item.kind !== 'onlineUsersRoot') return []
+ const items = this.onlineUsers
+ .values()
+ .map(user => ({ kind: 'onlineUser', user }) satisfies PanelItem)
+ .toArray()
+ items.sort((a, b) => a.user.name.localeCompare(b.user.name))
+ return items
+ }
+
+ dispose() {
+ for (const d of this.disposables) d.dispose()
+ this.disposables.length = 0
+ this.onDidChangeTreeDataEmitter.dispose()
+ }
+}
diff --git a/vscode-workbench/src/remoteDoc.ts b/vscode-workbench/src/remoteDoc.ts
deleted file mode 100644
index f26babc..0000000
--- a/vscode-workbench/src/remoteDoc.ts
+++ /dev/null
@@ -1,72 +0,0 @@
-import { HocuspocusProvider, type HocuspocusProviderWebsocket, type onSyncedParameters } from '@hocuspocus/provider'
-import vs from 'vscode'
-import * as Y from 'yjs'
-
-/** Manages per-doc connections to `collab-server`.
- * We refer to collaborative text buffers as 'docs', matching Yjs's `Y.Doc`.
- * Docs are addressed by file paths but exist in `collab-server`'s memory.
- * Docs can be open despite not having an underlying file
- * (e.g. when one person removes a file that others still have open).
- * They are only written to the filesystem when users save. */
-export class RemoteDocManager implements vs.Disposable {
- /** absolute path ↦ remote doc connection */
- private hpPromises = new Map>()
-
- constructor(
- private readonly collabSock: HocuspocusProviderWebsocket,
- private readonly log: vs.LogOutputChannel,
- ) {}
-
- /** Return the remote connection if one has already been started for the given file path.
- * Waits for initial sync but does not initiate a new connection. */
- async getStartedDoc(filePath: string): Promise {
- return this.hpPromises.get(filePath)
- }
-
- /** Return the remote connection for the given file path.
- * Waits for initial sync of buffer contents before returning. */
- // TODO: when do we close a remote doc? `onDidCloseTextDocument`?
- async ensureDoc(filePath: string): Promise {
- let p = this.hpPromises.get(filePath)
- if (!p) {
- p = new Promise((resolve, reject) => {
- // https://tiptap.dev/docs/hocuspocus/provider/examples#multiplexing
- const hp = new HocuspocusProvider({
- websocketProvider: this.collabSock,
- name: filePath,
- })
- const timer = setTimeout(() => {
- hp.destroy()
- if (this.hpPromises.get(filePath) === p) this.hpPromises.delete(filePath)
- reject(new Error(`[HocuspocusProvider] '${filePath}' timed out before initial sync`))
- }, 3_000)
- const onInitialSync = (data?: onSyncedParameters) => {
- clearTimeout(timer)
- hp.off('synced', onInitialSync)
- this.log.trace(`[HocuspocusProvider] '${filePath}' synced ${data ? String(data.state) : ''}`)
- resolve(hp)
- }
- if (hp.synced) onInitialSync()
- else hp.on('synced', onInitialSync)
- hp.attach()
- })
- this.hpPromises.set(filePath, p)
- }
- return (await p).document
- }
-
- /** Signal `collab-server` to save the contents of the given doc. */
- async saveDoc(filePath: string) {
- const p = this.hpPromises.get(filePath)
- if (!p) return
- const hp = await p
- hp.sendStateless(JSON.stringify({ action: 'save' }))
- }
-
- dispose() {
- for (const p of this.hpPromises.values()) {
- void p.then(hp => hp.destroy()).catch(() => {})
- }
- this.hpPromises.clear()
- }
-}
diff --git a/vscode-workbench/src/remoteSelections.ts b/vscode-workbench/src/remoteSelections.ts
new file mode 100644
index 0000000..231e1ef
--- /dev/null
+++ b/vscode-workbench/src/remoteSelections.ts
@@ -0,0 +1,149 @@
+import vs from 'vscode'
+import { Awareness } from 'y-protocols/awareness'
+import { AWARENESS_SELECTION_KEY, AWARENESS_USER_KEY, AwarenessSelection, AwarenessUser } from './util'
+
+interface AwarenessState {
+ [AWARENESS_USER_KEY]: AwarenessUser
+ [AWARENESS_SELECTION_KEY]: AwarenessSelection
+}
+
+class ClientDecorations implements vs.Disposable {
+ readonly cursorBefore: vs.TextEditorDecorationType
+ readonly cursorAfter: vs.TextEditorDecorationType
+
+ constructor(color: string) {
+ const selectionStyle: vs.DecorationRenderOptions = {
+ backgroundColor: `${color}40`,
+ rangeBehavior: vs.DecorationRangeBehavior.ClosedClosed,
+ overviewRulerColor: color,
+ overviewRulerLane: vs.OverviewRulerLane.Center,
+ }
+ const cursorStyle: vs.ThemableDecorationAttachmentRenderOptions = {
+ contentText: '',
+ border: `1px solid ${color}`,
+ margin: '0px -1px',
+ }
+ this.cursorBefore = vs.window.createTextEditorDecorationType({
+ ...selectionStyle,
+ before: cursorStyle,
+ })
+ this.cursorAfter = vs.window.createTextEditorDecorationType({
+ ...selectionStyle,
+ after: cursorStyle,
+ })
+ }
+
+ dispose() {
+ this.cursorBefore.dispose()
+ this.cursorAfter.dispose()
+ }
+}
+
+/** Listens for awareness changes from other clients
+ * (see `textBinding.ts` for the sending side)
+ * and shows remote selections as decorations in the appropriate editor view. */
+export class RemoteSelectionDecorator implements vs.Disposable {
+ private readonly localClientId: number
+ private readonly decorationTypes = new Map()
+ private states = new Map()
+ private readonly disposables: vs.Disposable[] = []
+
+ constructor(private readonly awareness: Awareness) {
+ this.localClientId = awareness.clientID
+ const onAwarenessChange = () => this.onAwarenessChange()
+ awareness.on('change', onAwarenessChange)
+ this.disposables.push(
+ { dispose: () => awareness.off('change', onAwarenessChange) },
+ // Redraw indicators on editor visibility changes, too.
+ vs.window.onDidChangeVisibleTextEditors(() => this.render()),
+ vs.window.onDidChangeTextEditorSelection(e => {
+ if (e.textEditor.document.uri.scheme !== 'file') return
+ this.awareness.setLocalStateField(AWARENESS_SELECTION_KEY, {
+ filePath: e.textEditor.document.uri.fsPath,
+ // FIXME: use LSP types
+ selections: e.selections.map(s => ({
+ anchor: { line: s.anchor.line, character: s.anchor.character },
+ active: { line: s.active.line, character: s.active.character },
+ })),
+ } satisfies AwarenessSelection)
+ }),
+ vs.workspace.onDidCloseTextDocument(doc => {
+ if (doc.uri.scheme !== 'file') return
+ // If cursor was in the now-closed doc, clear it.
+ const sel = this.awareness.getLocalState()?.[AWARENESS_SELECTION_KEY] as AwarenessSelection | undefined
+ if (sel?.filePath === doc.uri.fsPath) {
+ this.awareness.setLocalStateField(AWARENESS_SELECTION_KEY, null)
+ }
+ }),
+ )
+ this.onAwarenessChange()
+ }
+
+ private decorationsFor(clientId: number, color: string): ClientDecorations {
+ let decos = this.decorationTypes.get(clientId)
+ if (!decos) {
+ decos = new ClientDecorations(color)
+ this.decorationTypes.set(clientId, decos)
+ }
+ return decos
+ }
+
+ private onAwarenessChange(): void {
+ const states = this.awareness.getStates()
+ const next = new Map()
+ for (const [clientId, state] of states.entries()) {
+ if (clientId === this.localClientId) continue
+ const selection = state[AWARENESS_SELECTION_KEY] as AwarenessSelection | undefined
+ const user = state[AWARENESS_USER_KEY] as AwarenessUser | undefined
+ if (!selection || !user) continue
+ next.set(clientId, { selection, user })
+ }
+ // Drop decoration types for clients that are gone.
+ for (const [clientId, decos] of this.decorationTypes) {
+ if (next.has(clientId)) continue
+ decos.dispose()
+ this.decorationTypes.delete(clientId)
+ }
+ this.states = next
+ this.render()
+ }
+
+ private render(): void {
+ for (const editor of vs.window.visibleTextEditors) {
+ if (editor.document.uri.scheme !== 'file') continue
+ const filePath = editor.document.uri.fsPath
+ for (const [clientId, { selection, user }] of this.states) {
+ const decos = this.decorationsFor(clientId, user.color)
+ const beforeRanges: vs.DecorationOptions[] = []
+ const afterRanges: vs.DecorationOptions[] = []
+ if (selection?.filePath === filePath) {
+ for (const s of selection.selections) {
+ const range = new vs.Range(s.anchor.line, s.anchor.character, s.active.line, s.active.character)
+ const opts = { range, hoverMessage: user?.name }
+ // Is `active` at the start or the end of the selection?
+ if (
+ s.active.line < s.anchor.line ||
+ (s.active.line === s.anchor.line && s.active.character < s.anchor.character)
+ ) {
+ beforeRanges.push(opts)
+ } else {
+ afterRanges.push(opts)
+ }
+ }
+ }
+ editor.setDecorations(decos.cursorBefore, beforeRanges)
+ editor.setDecorations(decos.cursorAfter, afterRanges)
+ }
+ }
+ }
+
+ dispose(): void {
+ for (const d of this.disposables) d.dispose()
+ this.disposables.length = 0
+ for (const decos of this.decorationTypes.values()) {
+ decos.dispose()
+ }
+ this.decorationTypes.clear()
+ this.states.clear()
+ }
+}
diff --git a/vscode-workbench/src/textBinding.ts b/vscode-workbench/src/textBinding.ts
index 34d039d..1b3d116 100644
--- a/vscode-workbench/src/textBinding.ts
+++ b/vscode-workbench/src/textBinding.ts
@@ -1,17 +1,17 @@
+import { HocuspocusProvider, HocuspocusProviderWebsocket } from '@hocuspocus/provider'
import path from 'node:path'
import vs from 'vscode'
import * as Y from 'yjs'
-import { RemoteDocManager } from './remoteDoc'
-import { YTEXT_KEY } from './util'
+import { Logger, logWithPrefix, YTEXT_KEY } from './util'
/** Maintains a {@link YTextBinding} binding for every open {@link vs.TextDocument}
* whose path lies within one of the syncable directories. */
export class YTextBindingManager implements vs.Disposable {
- private bindings = new Map>()
+ private bindings = new Map()
private disposables: vs.Disposable[] = []
constructor(
- private readonly docs: RemoteDocManager,
+ private readonly collabSock: HocuspocusProviderWebsocket,
/** Directories to sync. Files not contained in any of these are not synced. */
private syncDirs: string[],
private readonly log: vs.LogOutputChannel,
@@ -29,10 +29,10 @@ export class YTextBindingManager implements vs.Disposable {
updateSyncableDirs(syncDirs: string[]) {
this.syncDirs = syncDirs
// Tear down bindings no longer in any syncable dir
- for (const [filePath, entry] of this.bindings) {
+ for (const [filePath, binding] of this.bindings) {
if (this.shouldSyncPath(filePath)) continue
this.bindings.delete(filePath)
- void entry.then(hp => hp?.dispose())
+ binding.dispose()
}
// Rebind already-open buffers in case they are now syncable
// (no-op if already bound)
@@ -52,149 +52,404 @@ export class YTextBindingManager implements vs.Disposable {
if (!this.shouldSyncPath(filePath)) return
// TODO: can one path have multiple `TextDocument`s?
if (this.bindings.has(filePath)) return
- const remoteDoc = this.docs.ensureDoc(filePath)
- const promise = remoteDoc
- .then(rd => new YTextBinding(doc, rd, this.log))
- .catch(err => {
- this.log.error(`[onDidOpenTextDocument] failed to initialize Yjs binding for '${filePath}': ${String(err)}`)
- if (this.bindings.get(filePath) === promise) this.bindings.delete(filePath)
- return undefined
- })
- this.bindings.set(filePath, promise)
+ this.bindings.set(filePath, new YTextBinding(doc, this.collabSock, this.log))
}
private onDidCloseTextDocument(doc: vs.TextDocument) {
if (doc.uri.scheme !== 'file') return
const filePath = doc.uri.fsPath
- const entry = this.bindings.get(filePath)
- if (!entry) return
+ const binding = this.bindings.get(filePath)
+ if (!binding) return
this.bindings.delete(filePath)
- void entry.then(hp => hp?.dispose())
+ binding.dispose()
}
private onDidChangeTextDocument(e: vs.TextDocumentChangeEvent) {
if (e.document.uri.scheme !== 'file') return
const filePath = e.document.uri.fsPath
- const entry = this.bindings.get(filePath)
- if (!entry) {
+ const binding = this.bindings.get(filePath)
+ if (!binding) {
if (this.shouldSyncPath(filePath)) {
this.log.warn(`[onDidChangeTextDocument] dropped edit on '${filePath}', missing YTextBinding`)
}
return
}
- void entry.then(hp => hp?.onLocalChange(e))
+ binding.onLocalChange(e)
}
dispose() {
for (const d of this.disposables) d.dispose()
this.disposables = []
- for (const b of this.bindings.values()) void b.then(hp => hp?.dispose())
+ for (const b of this.bindings.values()) b.dispose()
this.bindings.clear()
}
}
-/** Bidirectional binding between a {@link vs.TextDocument} and a {@link Y.Doc}. */
+/** Common interface between {@link vs.TextEditorEdit} and {@link vs.WorkspaceEdit}. */
+interface EditBuilder {
+ insert(location: vs.Position, newText: string): void
+ delete(location: vs.Range): void
+ replace(range: vs.Range, newText: string): void
+}
+
+/** Bidirectional binding between a {@link vs.TextDocument}
+ * and the {@link Y.Text} of a {@link HocuspocusProvider}.
+ *
+ * WARNING: Unlike Monaco, VSCode has no API for synchronous edits.
+ * This binding is correspondingly much more subtle than Y-Monaco.
+ * When a remote change comes in,
+ * we repeatedly attempt to apply it as an asynchronous edit;
+ * an attempt may fail if a local change is made in the meantime.
+ * To compute the correct edit w.r.t. the current document contents,
+ * we diff the `remoteYtext` that contains remote changes
+ * against our `localYtext` that matches the VSCode-managed `doc`.
+ *
+ * The synchronization flow of a single change is:
+ * ```mermaid
+ * flowchart TB
+ * subgraph Alice["Alice's extensionHost"]
+ * ADoc["vscode.TextDocument"]
+ * AYjsL["local Y.Doc"]
+ * AYjsR["remote Y.Doc"]
+ * ADoc -->|"YTextBinding.onLocalChange"| AYjsL
+ * AYjsL -->|"YTextBinding.onLocalUpdate"| AYjsR
+ * end
+
+ * subgraph Bob["Bob's extensionHost"]
+ * BDoc["vscode.TextDocument"]
+ * BYjsL["local Y.Doc"]
+ * BYjsR["remote Y.Doc"]
+ * BYjsR -->|"YTextBinding.mergeRemoteDiff"| BDoc & BYjsL
+ * end
+
+ * subgraph Server["collab-server"]
+ * CYjs["collab Y.Doc"]
+ * end
+
+ * AYjsR -->|"sync"| CYjs
+ * CYjs -->|"sync"| BYjsR
+ * ```
+ */
export class YTextBinding implements vs.Disposable {
- private ytext: Y.Text
- /** Used to prevent `applyEdit` bounceback when applying remote changes;
- * when set, local `onDidChangeTextDocument` events are ignored. */
- // FIXME: try hard to hack through vscode and tag edit events. Would be much simpler.
- private applyingRemote = false
- /** Used to linearize async operations that might otherwise interleave. */
- private pending: Promise = Promise.resolve()
+ private readonly hs: HocuspocusProvider
+
+ /** Public for tests only. */
+ get remoteYtext(): Y.Text {
+ return this.hs.document.getText(YTEXT_KEY)
+ }
- private disposables: { dispose(): unknown }[] = []
+ /** The CRDT that we base remote diffs on (see comment above).
+ * - Defined from initial sync onwards.
+ * - Inbetween {@link mutex}-guarded transactions,
+ * its contents must match those of {@link doc}.
+ * - Includes a subset of the updates seen by {@link hs}. */
+ private localYdoc: Y.Doc | undefined
+
+ /** True once we have received an initial remote doc from the collab-server.
+ * Public for tests only. */
+ get initialSyncDone(): boolean {
+ return !!this.localYdoc
+ }
+
+ private get localYtext(): Y.Text {
+ return this.localYdoc!.getText(YTEXT_KEY)
+ }
+
+ private ensureSyncTimeout: NodeJS.Timeout | undefined
+
+ /** Used to linearize and order async operations
+ * that temporarily create inconsistent states while suspended. */
+ private mutex: Promise = Promise.resolve()
+
+ private readonly log: Logger
- /** May only be constructed with a `Y.Doc` whose provider has already `synced` at least once. */
constructor(
readonly doc: vs.TextDocument,
- readonly remoteDoc: Y.Doc,
- private readonly log: vs.LogOutputChannel,
+ collabSock: HocuspocusProviderWebsocket,
+ log_: Logger,
+ /** The timeout period for {@link scheduleEnsureSync} in milliseconds,
+ * disabling {@link scheduleEnsureSync} if zero.
+ * Expected to be non-zero except in tests. */
+ private readonly ensureSyncTimeoutMs: number = 3_000,
+ /** Name of this document in {@link collabSock}.
+ * Expected to be the file path except in tests. */
+ docName: string = doc.uri.fsPath,
) {
- this.ytext = remoteDoc.getText(YTEXT_KEY)
+ // https://tiptap.dev/docs/hocuspocus/provider/examples#multiplexing
+ this.hs = new HocuspocusProvider({
+ websocketProvider: collabSock,
+ name: docName,
+ // We use a single, global awareness CRDT rather than per-document CRDTs.
+ awareness: null,
+ })
+ this.hs.attach()
+
+ this.log = logWithPrefix(log_, `[YTextBinding(${docName}|${this.hs.document.clientID.toString(16)})]`)
- // Overwrite with remote contents on startup.
- this.enqueue(() => this.replaceWithRemote())
+ this.remoteYtext.observe(this.onRemoteUpdate)
- const observer = (event: Y.YTextEvent, transaction: Y.Transaction) => {
- // Prevent bounceback (https://beta.yjs.dev/docs/api/transactions/#the-origin-concept).
- if (transaction.origin === this) return
- const delta = event.delta
- this.enqueue(() => this.applyDelta(delta))
+ const onLaterSync = () => {
+ this.log.warn(`unexpected reconnection from collab-server`)
+ }
+ if (this.hs.synced) {
+ this.enqueueTransaction(() => this.initFromRemote())
+ this.hs.on('synced', onLaterSync)
+ } else {
+ const onInitialSync = () => {
+ this.hs.off('synced', onInitialSync)
+ this.enqueueTransaction(() => this.initFromRemote())
+ this.hs.on('synced', onLaterSync)
+ }
+ this.hs.on('synced', onInitialSync)
}
- this.ytext.observe(observer)
- this.disposables.push({
- dispose: () => {
- this.ytext.unobserve(observer)
- },
- })
}
/** Place an operation on the work queue.
* Work items are atomic w.r.t. all other work items
* (but not w.r.t. other `async` operations). */
- private enqueue(work: () => Promise): void {
- this.pending = this.pending.then(work).catch(e => {
- this.log.error(`[YTextBinding(${this.doc.uri.fsPath})] ${String(e)}`)
+ private enqueueTransaction(work: () => Promise): void {
+ this.mutex = this.mutex.then(work).catch(e => {
+ this.log.error(e)
})
}
+ /** Attempt to make a local edit. Return `true` iff successful. */
+ private async makeLocalEdit(fn: (_: EditBuilder) => void): Promise {
+ const MAX_EDITOR_RETRIES = 10
+ const MAX_WORKSPACE_RETRIES = 10
+
+ /** First try {@link vs.TextEditor.edit}.
+ * Preferrable because it has a version guard:
+ * `fn` runs with a given {@link vs.TextDocument.version}
+ * and the resulting edit is rejected if the doc moves in the meantime,
+ * guaranteeing correct offsets.
+ * Needs the document to be open in a visible editor. */
+ for (let i = 0; i < MAX_EDITOR_RETRIES; i++) {
+ let hasEditor = false
+ for (const e of vs.window.visibleTextEditors) {
+ if (e.document === this.doc) {
+ hasEditor = true
+ const success = await e.edit(fn)
+ if (success) {
+ this.log.trace('[makeLocalEdit] used TextEditor.edit')
+ return true
+ }
+ }
+ }
+ if (!hasEditor) break
+ }
+
+ /** Then try {@link vs.WorkspaceEdit}.
+ * No version guard so can't handle concurrent local edits,
+ * but generally only runs if the document is not being actively edited
+ * (except for very rare races with programmatic edits). */
+ for (let i = 0; i < MAX_WORKSPACE_RETRIES; i++) {
+ const edit = new vs.WorkspaceEdit()
+ fn({
+ insert: (l, t) => edit.insert(this.doc.uri, l, t),
+ delete: r => edit.delete(this.doc.uri, r),
+ replace: (r, t) => edit.replace(this.doc.uri, r, t),
+ })
+ const success = await vs.workspace.applyEdit(edit)
+ if (success) {
+ this.log.trace('[makeLocalEdit] used workspace.applyEdit')
+ return true
+ }
+ }
+ return false
+ }
+
+ /** (Re)initialize {@link localYdoc} and {@link doc} with the remote text,
+ * replacing the entire {@link doc} buffer if necessary.
+ * Avoids making an edit when contents already match. */
+ private async initFromRemote(): Promise {
+ if (this.localYdoc) {
+ this.localYdoc.off('update', this.onLocalUpdate)
+ this.localYdoc.destroy()
+ }
+ this.localYdoc = new Y.Doc()
+ Y.applyUpdate(this.localYdoc, Y.encodeStateAsUpdate(this.hs.document))
+ this.localYdoc.on('update', this.onLocalUpdate)
+
+ const remoteStr = this.remoteYtext.toString()
+ const localStr = this.doc.getText()
+ let success = false
+ if (remoteStr === localStr) {
+ success = true
+ } else {
+ success = await this.makeLocalEdit(b => {
+ const fullRange = new vs.Range(new vs.Position(0, 0), this.doc.positionAt(this.doc.getText().length))
+ b.replace(fullRange, remoteStr)
+ })
+ }
+ if (success) {
+ this.log.trace('[initFromRemote] synced')
+ } else {
+ this.log.error(`[initFromRemote] failed to overwrite document`)
+ }
+ }
+
+ private onRemoteUpdate = (_: Y.YTextEvent, transaction: Y.Transaction) => {
+ // First check prevents bounceback (https://beta.yjs.dev/docs/api/transactions/#the-origin-concept).
+ // Second ignores remote deltas before remote doc has been received.
+ if (transaction.origin === this || !this.initialSyncDone) return
+ this.scheduleMergeRemoteDiff()
+ }
+
+ /** Event handler for `this.localYDoc.on('update')`. */
+ private onLocalUpdate = (update: Uint8Array, origin: unknown) => {
+ // On the local doc, `origin === this` means *do broadcast*.
+ if (origin !== this || !this.initialSyncDone) return
+
+ /** Apply this broadcastable local change to the remote doc.
+ * Crucial to make edits on local Y.doc in {@link onLocalChange} and propagate the update to remote
+ * rather than the other way around:
+ * in general, remote has seen more updates than local,
+ * so an update generated on the remote CRDT may have overly recent clocks,
+ * thus being stashed in the local doc's `pendingStructs`
+ * rather than being immediately applied.
+ * This would lead it to produce deltas duplicating local changes in {@link mergeRemoteDiff}. */
+ Y.applyUpdate(this.hs.document, update, this)
+ }
+
onLocalChange(e: vs.TextDocumentChangeEvent): void {
- // BUG 1: local edits that arrive while `applyingRemote` is set,
- // if that is possible, are lost.
- // would also linearizing `onLocalChange` help?
- if (this.applyingRemote) return
- if (e.document !== this.doc) return
- if (e.contentChanges.length === 0) return
- this.remoteDoc.transact(() => {
+ if (e.document !== this.doc) throw new Error('internal error: received event for wrong document')
+ if (!this.initialSyncDone || e.contentChanges.length === 0) return
+ if (!e.detailedReason) throw new Error('internal error: textDocumentChangeReason API proposal is disabled')
+ // File re-read from disk
+ if (e.detailedReason.source === 'reloadFromDisk') {
+ // Prefer CRDT state to on-disk contents
+ this.scheduleEnsureSync()
+ return
+ }
+ /** Prevent loopback by checking for the two methods of editing used in {@link makeLocalEdit}. */
+ if (
+ e.detailedReason.source === 'unknown' &&
+ e.detailedReason.metadata.source === 'unknown' &&
+ (!e.detailedReason.metadata.name /* workspace.applyEdit */ ||
+ e.detailedReason.metadata.name === 'pushEditOperation' /* workspace.applyEdit */ ||
+ e.detailedReason.metadata.name === 'MainThreadTextEditor') /* TextEditor.edit */
+ ) {
+ // TODO these checks are *incomplete*:
+ // we must not broadcast our applications of remote changes
+ // (since that would cause an infinite broadcast loop),
+ // but we should broadcast programmatic edits from other extensions
+ // (notably Vim and VSCode Neovim).
+ // However, there is no VSCode API to set the `detailedReason`,
+ // or any other field of the resulting `TextDocumentChangeEvent`,
+ // and checking document versions or edit content
+ // turned out prone to a number of race conditions.
+ // The only viable fix seems to be patching `openvscode-server`
+ // to support setting `detailedReason.source` on our own edits.
+ // For now, {@link scheduleEnsureSync} reverts unbroadcasted local changes.
+ this.scheduleEnsureSync()
+ return
+ }
+
+ this.log.trace(
+ `[onLocalChange] broadcasting ${JSON.stringify(e.contentChanges.map(c => [c.rangeOffset, c.rangeLength, c.text]))} (detailed reason ${JSON.stringify(e.detailedReason)})`,
+ )
+
+ /** Apply the broadcastable local change to {@link localYdoc} with `this` origin.
+ * (Remote changes are applied to {@link localYdoc} in {@link mergeRemoteDiff}.) */
+ this.localYdoc!.transact(() => {
// VSCode sorts `contentChanges` in reverse offset order
// so they can be applied sequentially without offset adjustment.
for (const ch of e.contentChanges) {
- if (ch.rangeLength) this.ytext.delete(ch.rangeOffset, ch.rangeLength)
- if (ch.text) this.ytext.insert(ch.rangeOffset, ch.text)
+ if (ch.rangeLength) this.localYtext.delete(ch.rangeOffset, ch.rangeLength)
+ if (ch.text) this.localYtext.insert(ch.rangeOffset, ch.text)
}
}, this)
+ this.scheduleEnsureSync()
+ }
+
+ /** Whether a run of {@link mergeRemoteDiff} is already scheduled.
+ * Used to avoid running many redundant merges with empty deltas. */
+ private mergeRemoteDiffScheduled: boolean = false
+
+ private scheduleMergeRemoteDiff(): void {
+ if (this.mergeRemoteDiffScheduled) return
+ this.enqueueTransaction(() => this.mergeRemoteDiff())
+ this.mergeRemoteDiffScheduled = true
}
- private async applyDelta(delta: Y.YTextEvent['delta']): Promise {
- const edit = new vs.WorkspaceEdit()
- let offset = 0
- for (const op of delta) {
- if (op.retain != null) {
- offset += op.retain
- } else if (op.delete != null) {
- edit.delete(this.doc.uri, new vs.Range(this.doc.positionAt(offset), this.doc.positionAt(offset + op.delete)))
- offset += op.delete
- } else if (typeof op.insert === 'string') {
- edit.insert(this.doc.uri, this.doc.positionAt(offset), op.insert)
+ private async mergeRemoteDiff(): Promise {
+ this.mergeRemoteDiffScheduled = false
+ let update: Uint8Array | undefined
+ const mkEdits = (b: EditBuilder) => {
+ // Observe the delta by updating a fresh Y.Doc
+ // (there is no way to compute a delta from an update directly).
+ const fork = new Y.Doc()
+ Y.applyUpdate(fork, Y.encodeStateAsUpdate(this.localYdoc!))
+ // Yjs fires observers synchronously, thus populating `delta`, during `applyUpdate`.
+ let delta: Y.YTextEvent['delta'] = []
+ fork.getText(YTEXT_KEY).observe(e => {
+ delta = e.delta
+ })
+ update = Y.encodeStateAsUpdate(this.hs.document)
+ Y.applyUpdate(fork, update)
+ fork.destroy()
+ if (delta.length === 0) return
+
+ this.log.trace(`[mergeRemoteDiff] applying delta ${JSON.stringify(delta)}`)
+ let offset = 0
+ for (const op of delta) {
+ if (typeof op.retain === 'number') {
+ offset += op.retain
+ } else if (typeof op.delete === 'number') {
+ b.delete(new vs.Range(this.doc.positionAt(offset), this.doc.positionAt(offset + op.delete)))
+ offset += op.delete
+ } else if (typeof op.insert === 'string') {
+ // Ignoring `op.insert : object | Y.AbstractType`
+ b.insert(this.doc.positionAt(offset), op.insert)
+ }
}
}
- this.applyingRemote = true
- try {
- await vs.workspace.applyEdit(edit)
- } finally {
- this.applyingRemote = false
+
+ const success = await this.makeLocalEdit(mkEdits)
+ if (success) {
+ if (!update) throw new Error('[mergeRemoteDiff] internal error: edit succeeded but update missing')
+ // Edit is now included in `doc`, update `localYdoc` to match.
+ Y.applyUpdate(this.localYdoc!, update)
+ } else {
+ this.log.warn(`[mergeRemoteDiff] edit failed, dropping update`)
}
+ this.scheduleEnsureSync()
}
- /** Ensure that buffer contents match the Y.Doc text
- * by replacing the entire buffer if necessary.
- * Avoids making an edit when contents already match. */
- async replaceWithRemote() {
- const ytextStr = this.ytext.toString()
- if (ytextStr === this.doc.getText()) return
- const edit = new vs.WorkspaceEdit()
- const fullRange = new vs.Range(new vs.Position(0, 0), this.doc.positionAt(this.doc.getText().length))
- edit.replace(this.doc.uri, fullRange, ytextStr)
- this.applyingRemote = true
- try {
- await vs.workspace.applyEdit(edit)
- } finally {
- this.applyingRemote = false
- }
+ /** Ensure that {@link localYdoc} has the same contents as {@link doc},
+ * and that {@link localYdoc} and {@link hs} have the same CRDT state.
+ * Overwrite {@link localYdoc} and {@link doc} if this is not the case.
+ * Debounced - runs {@link ensureSyncTimeoutMs} after the most recent invocation. */
+ private scheduleEnsureSync() {
+ if (!this.initialSyncDone || this.ensureSyncTimeoutMs === 0) return
+ if (this.ensureSyncTimeout) clearTimeout(this.ensureSyncTimeout)
+ this.ensureSyncTimeout = setTimeout(() => {
+ this.enqueueTransaction(async () => {
+ const localYtextStr = this.localYtext.toString()
+ const docStr = this.doc.getText()
+ if (docStr !== localYtextStr) {
+ this.log.debug('[ensureSync] doc<->localYdoc desync, overwriting')
+ await this.initFromRemote()
+ return
+ }
+ const sl = Y.encodeStateVector(this.localYdoc!)
+ const sr = Y.encodeStateVector(this.hs.document)
+ if (sl.length !== sr.length || !sl.every((b, i) => b === sr[i])) {
+ this.log.debug('[ensureSync] remoteYdoc<->localYdoc desync, overwriting')
+ await this.initFromRemote()
+ }
+ })
+ }, this.ensureSyncTimeoutMs)
}
dispose() {
- for (const d of this.disposables) d.dispose()
+ clearTimeout(this.ensureSyncTimeout)
+
+ this.localYdoc?.off('update', this.onLocalUpdate)
+ this.localYdoc?.destroy()
+
+ this.remoteYtext.unobserve(this.onRemoteUpdate)
+ this.hs.destroy()
}
}
diff --git a/vscode-workbench/src/util.ts b/vscode-workbench/src/util.ts
index e5d3f60..417a169 100644
--- a/vscode-workbench/src/util.ts
+++ b/vscode-workbench/src/util.ts
@@ -1,11 +1,110 @@
+import fs from 'node:fs/promises'
+import vs from 'vscode'
+import { z } from 'zod'
+
+/** Subset of {@link vs.LogOutputChannel} used for our purposes. */
+export type Logger = Pick
+
+/** Wrap `log` so that every message is prepended with `prefix`. */
+export function logWithPrefix(log: Logger, prefix: string): Logger {
+ class PrefixedLogger {
+ get logLevel() {
+ return log.logLevel
+ }
+ trace(msg: string, ...args: unknown[]) {
+ log.trace(`${prefix} ${msg}`, ...args)
+ }
+ debug(msg: string, ...args: unknown[]) {
+ log.debug(`${prefix} ${msg}`, ...args)
+ }
+ info(msg: string, ...args: unknown[]) {
+ log.info(`${prefix} ${msg}`, ...args)
+ }
+ warn(msg: string, ...args: unknown[]) {
+ log.warn(`${prefix} ${msg}`, ...args)
+ }
+ error(msg: string | Error, ...args: unknown[]) {
+ log.error(`${prefix} ${String(msg)}`, ...args)
+ }
+ }
+ return new PrefixedLogger()
+}
+
+export function equalMaps(a: Map, b: Map, eqU?: (a: U, b: U) => boolean): boolean {
+ if (a.size !== b.size) return false
+ for (const [id, u] of a) {
+ if (!b.has(id)) return false
+ const v = b.get(id) as U
+ if (eqU ? !eqU(v, u) : v !== u) return false
+ }
+ return true
+}
+
// FIXME: use same consts in workbench-app/collab-server for single source of truth.
+/** Path to workspace metadata file in VSCode bwraps. */
+export const BWRAP_METADATA_PATH = '/workspace/.lean-workbench.json'
+
+export const zWorkspaceMetadata = z.object({
+ /** Name of the user viewing/editing the project. */
+ viewer: z.object({
+ name: z.string(),
+ image: z.nullish(z.string()),
+ }),
+})
+
+/** Metadata of a Lean Workbench project workspace. */
+export type WorkspaceMetadata = z.infer
+
/** Working directory of collab-server in the VSCode and collab-server bwraps. */
export const BWRAP_COLLAB_SERVER_DIR = '/workspace/.collab-server'
/** Collab-server socket path in the VSCode and collab-server bwraps. */
export const BWRAP_COLLAB_SOCK_PATH = `${BWRAP_COLLAB_SERVER_DIR}/collab.sock`
-/** We keep a unique Y.Doc per file.
+/** We keep a Y.Doc per collaboratively-editable file.
* This is the Y.Doc key under which the text content lives. */
export const YTEXT_KEY = 'content'
+
+export interface Position {
+ line: number
+ character: number
+}
+
+export interface Selection {
+ anchor: Position
+ active: Position
+}
+
+export interface AwarenessUser {
+ name: string
+ color: string
+ image?: string | null
+}
+
+export function equalAwarenessUsers(u: AwarenessUser, v: AwarenessUser): boolean {
+ return v.name === u.name && v.color === u.color && v.image === u.image
+}
+
+export const AWARENESS_DOC_NAME = ''
+export const AWARENESS_USER_KEY = 'user'
+export const AWARENESS_SELECTION_KEY = 'selection'
+/** Colors for remote collaborator cursors. */
+export const AWARENESS_CURSOR_COLORS = ['#5790FC', '#F89C20', '#E42536', '#964A8B', '#9C9CA1', '#7A21DD']
+
+export interface AwarenessSelection {
+ filePath: string
+ selections: Selection[]
+}
+
+export async function waitForPath(p: string, timeoutMs: number): Promise {
+ const deadline = Date.now() + timeoutMs
+ while (Date.now() < deadline) {
+ try {
+ await fs.access(p)
+ return true
+ } catch {}
+ await new Promise(r => setTimeout(r, 200))
+ }
+ return false
+}
diff --git a/vscode-workbench/src/vscode.proposed.extensionsAny.d.ts b/vscode-workbench/src/vscode.proposed.extensionsAny.d.ts
new file mode 100644
index 0000000..caaffee
--- /dev/null
+++ b/vscode-workbench/src/vscode.proposed.extensionsAny.d.ts
@@ -0,0 +1,43 @@
+/*---------------------------------------------------------------------------------------------
+ * Copyright (c) Microsoft Corporation. All rights reserved.
+ * Licensed under the MIT License. See License.txt in the project root for license information.
+ *--------------------------------------------------------------------------------------------*/
+
+declare module 'vscode' {
+ // https://github.com/microsoft/vscode/issues/145307 @alexdima
+
+ export interface Extension {
+ /**
+ * `true` when the extension is associated to another extension host.
+ *
+ * *Note* that an extension from another extension host cannot export
+ * API, e.g {@link Extension.exports its exports} are always `undefined`.
+ */
+ readonly isFromDifferentExtensionHost: boolean
+ }
+
+ export namespace extensions {
+ /**
+ * Get an extension by its full identifier in the form of: `publisher.name`.
+ *
+ * @param extensionId An extension identifier.
+ * @param includeDifferentExtensionHosts Include extensions from different extension host
+ * @return An extension or `undefined`.
+ */
+ export function getExtension(
+ extensionId: string,
+ includeDifferentExtensionHosts: boolean,
+ ): Extension | undefined
+ export function getExtension(
+ extensionId: string,
+ includeDifferentExtensionHosts: true,
+ ): Extension | undefined
+
+ /**
+ * All extensions across all extension hosts.
+ *
+ * @see {@link Extension.isFromDifferentExtensionHost}
+ */
+ export const allAcrossExtensionHosts: readonly Extension[]
+ }
+}
diff --git a/vscode-workbench/src/vscode.proposed.textDocumentChangeReason.d.ts b/vscode-workbench/src/vscode.proposed.textDocumentChangeReason.d.ts
new file mode 100644
index 0000000..8c25c8d
--- /dev/null
+++ b/vscode-workbench/src/vscode.proposed.textDocumentChangeReason.d.ts
@@ -0,0 +1,29 @@
+/*---------------------------------------------------------------------------------------------
+ * Copyright (c) Microsoft Corporation. All rights reserved.
+ * Licensed under the MIT License. See License.txt in the project root for license information.
+ *--------------------------------------------------------------------------------------------*/
+
+declare module 'vscode' {
+ /**
+ * Detailed information about why a text document changed.
+ */
+ export interface TextDocumentDetailedChangeReason {
+ /**
+ * The source of the change (e.g., 'inline-completion', 'chat-edit', 'extension')
+ */
+ readonly source: string
+
+ /**
+ * Additional context-specific metadata
+ */
+ readonly metadata: { readonly [key: string]: unknown }
+ }
+
+ export interface TextDocumentChangeEvent {
+ /**
+ * The precise reason for the document change.
+ * Only available to extensions that have enabled the `textDocumentChangeReason` proposed API.
+ */
+ readonly detailedReason: TextDocumentDetailedChangeReason | undefined
+ }
+}
diff --git a/vscode-workbench/test/collab.test.ts b/vscode-workbench/test/collab.test.ts
new file mode 100644
index 0000000..e4dacc7
--- /dev/null
+++ b/vscode-workbench/test/collab.test.ts
@@ -0,0 +1,221 @@
+import { HocuspocusProviderWebsocket } from '@hocuspocus/provider'
+import { Server } from '@hocuspocus/server'
+import * as assert from 'assert'
+import * as vs from 'vscode'
+import { YTextBinding } from '../src/textBinding'
+import { Logger } from '../src/util'
+
+const delay = (ms: number) => new Promise(r => setTimeout(r, ms))
+
+const logLevel: vs.LogLevel = vs.LogLevel.Debug as unknown as vs.LogLevel // cast prevents TS from complaining
+const consoleLog: Logger = {
+ logLevel,
+ trace: (m, ...a) => {
+ if (logLevel !== vs.LogLevel.Off && logLevel <= vs.LogLevel.Trace) console.log('[trace]', m, ...a)
+ },
+ debug: (m, ...a) => {
+ if (logLevel !== vs.LogLevel.Off && logLevel <= vs.LogLevel.Debug) console.log('[debug]', m, ...a)
+ },
+ info: (m, ...a) => {
+ if (logLevel !== vs.LogLevel.Off && logLevel <= vs.LogLevel.Info) console.log('[info]', m, ...a)
+ },
+ warn: (m, ...a) => {
+ if (logLevel !== vs.LogLevel.Off && logLevel <= vs.LogLevel.Warning) console.warn('[warn]', m, ...a)
+ },
+ error: (m, ...a) => {
+ if (logLevel !== vs.LogLevel.Off && logLevel <= vs.LogLevel.Error) console.error('[error]', String(m), ...a)
+ },
+}
+
+/** Small seeded PRNG (mulberry32) for reproducibility. */
+function mulberry32(seed: number): () => number {
+ let a = seed >>> 0
+ return () => {
+ a = (a + 0x6d2b79f5) | 0
+ let t = Math.imul(a ^ (a >>> 15), 1 | a)
+ t = (t + Math.imul(t ^ (t >>> 7), 61 | t)) ^ t
+ return ((t ^ (t >>> 14)) >>> 0) / 4294967296
+ }
+}
+
+const ALPHABET = 'abcdef \n'
+function randomText(rng: () => number, len: number): string {
+ let s = ''
+ for (let i = 0; i < len; i++) s += ALPHABET[Math.floor(rng() * ALPHABET.length)]
+ return s
+}
+
+/** Activate `doc` in `column`, then apply one random insert or delete
+ * by executing the `default:type` / `deleteLeft` commands on its editor. */
+async function randomEditOn(doc: vs.TextDocument, column: vs.ViewColumn, rng: () => number): Promise {
+ const editor = await vs.window.showTextDocument(doc, { viewColumn: column, preserveFocus: false, preview: false })
+ const len = doc.getText().length
+ const insert = len === 0 || rng() < 0.6
+ if (insert) {
+ const at = Math.floor(rng() * (len + 1))
+ editor.selection = new vs.Selection(doc.positionAt(at), doc.positionAt(at))
+ const text = randomText(rng, 1 + Math.floor(rng() * 6))
+ try {
+ await vs.commands.executeCommand('default:type', { text })
+ } catch (e) {
+ console.error('error on type', e)
+ }
+ } else {
+ const at = Math.floor(rng() * len)
+ const dl = 1 + Math.floor(rng() * Math.min(5, len - at))
+ editor.selection = new vs.Selection(doc.positionAt(at), doc.positionAt(at + dl))
+ try {
+ await vs.commands.executeCommand('deleteLeft')
+ } catch (e) {
+ console.error('error on deleteLeft', e)
+ }
+ }
+}
+
+/** Poll until the given {@link YTextBinding}s receive their remote docs. */
+async function waitForInitialSync(bindings: YTextBinding[], timeoutMs: number): Promise {
+ const deadline = performance.now() + timeoutMs
+ while (!bindings.every(b => b.initialSyncDone)) {
+ if (performance.now() >= deadline) {
+ assert.fail('timed out waiting for initial sync')
+ }
+ await delay(50)
+ }
+}
+
+/** Poll until the given {@link YTextBinding}s have remained unchanged for 1s. */
+async function waitForQuiescence(bindings: YTextBinding[], timeoutMs: number): Promise {
+ const deadline = performance.now() + timeoutMs
+ let prev = ''
+ let stableIters = 0
+ while (performance.now() < deadline) {
+ const snap = bindings.map(b => b.remoteYtext.toString() + '|' + b.doc.getText()).join('|')
+ if (snap === prev) {
+ if (stableIters++ >= 5) return
+ } else {
+ prev = snap
+ stableIters = 0
+ }
+ await delay(100)
+ }
+ assert.fail('timed out waiting for quiescent state')
+}
+
+function diffMessage(label: string, a: string, b: string): string {
+ let i = 0
+ while (i < a.length && i < b.length && a[i] === b[i]) i++
+ const ctx = (s: string) => JSON.stringify(s.slice(Math.max(0, i - 25), i + 25))
+ return `${label}: diverge at index ${i} (lenA=${a.length}, lenB=${b.length})\n A …${ctx(a)}…\n B …${ctx(b)}…`
+}
+
+const DOC_NAME = '/test/shared.txt'
+const COLUMNS: vs.ViewColumn[] = [vs.ViewColumn.One, vs.ViewColumn.Two]
+
+suite('Collaborative editing', () => {
+ interface TestHandles {
+ docs: vs.TextDocument[]
+ bindings: YTextBinding[]
+ dispose: () => Promise
+ }
+
+ const mkHandles = async (ensureSyncTimeoutMs: number = 0): Promise => {
+ // In-memory Hocuspocus server on an ephemeral port; no persistence, no signal handlers.
+ const server = new Server({ stopOnSignals: false, quiet: true })
+ await new Promise(resolve => server.httpServer.listen(0, '127.0.0.1', resolve))
+ const url = `ws://127.0.0.1:${server.address.port}`
+
+ const mkClient = () => new HocuspocusProviderWebsocket({ url })
+ const clients = [mkClient(), mkClient()]
+ const docs = await Promise.all([
+ vs.workspace.openTextDocument({ content: '', language: 'plaintext' }),
+ vs.workspace.openTextDocument({ content: '', language: 'plaintext' }),
+ ])
+ const bindings = docs.map((doc, i) => new YTextBinding(doc, clients[i], consoleLog, ensureSyncTimeoutMs, DOC_NAME))
+
+ // Route document changes to the matching binding
+ // (`YTextBindingManager.onDidChangeTextDocument` does this in production).
+ const changeSub = vs.workspace.onDidChangeTextDocument(e => {
+ const i = docs.indexOf(e.document)
+ if (i >= 0) bindings[i].onLocalChange(e)
+ })
+
+ return {
+ docs,
+ bindings,
+ dispose: async () => {
+ changeSub.dispose()
+ for (const b of bindings) b.dispose()
+ // Not disposing old docs to avoid 'did you mean to close unsaved buffer' warnings.
+ for (const c of clients) c.destroy()
+ await server.destroy()
+ },
+ }
+ }
+
+ test('YTextBindings reach initial sync', async function () {
+ const handles = await mkHandles()
+ await waitForInitialSync(handles.bindings, 1_000)
+ await handles.dispose()
+ })
+
+ test('Single edit propagates correctly', async function () {
+ const handles = await mkHandles()
+ await waitForInitialSync(handles.bindings, 1_000)
+
+ // Type on doc0 and confirm the change reaches doc1.
+ const ed0 = await vs.window.showTextDocument(handles.docs[0], { viewColumn: COLUMNS[0], preview: false })
+ ed0.selection = new vs.Selection(0, 0, 0, 0)
+ const text = 'PROBE\n'
+ await vs.commands.executeCommand('default:type', { text })
+ await waitForQuiescence(handles.bindings, 1_000)
+ assert.strictEqual(handles.docs[1].getText(), text)
+ await handles.dispose()
+ })
+
+ /** Drive a batch of edits, alternating between the two documents.
+ * Not waiting between edits opens a local-vs-remote change race window. */
+ const makeConcurrentEdits = async (handles: TestHandles) => {
+ const rng = mulberry32(0xc0ffee)
+ const NUM_EDITS = 100
+ for (let i = 0; i < NUM_EDITS; i++) {
+ await randomEditOn(handles.docs[i % 2], COLUMNS[i % 2], rng)
+ }
+ }
+
+ const assertEqualStates = (handles: TestHandles) => {
+ const [d0, d1] = handles.docs.map(d => d.getText())
+ const [y0, y1] = handles.bindings.map(b => b.remoteYtext.toString())
+
+ // Sanity check - YJs CRDT replicas converge.
+ assert.strictEqual(y0, y1, diffMessage('Y.Text replicas (client0 vs client1)', y0, y1))
+ // Whether docs correctly track CRDT replicas.
+ assert.strictEqual(d0, y0, diffMessage('doc0 vs its Y.Text', d0, y0))
+ assert.strictEqual(d1, y1, diffMessage('doc1 vs its Y.Text', d1, y1))
+ }
+
+ test('Concurrent edits settle on equal states', async function () {
+ this.timeout(20_000)
+ const ensureSyncTimeoutMs = 1_000
+ const handles = await mkHandles(ensureSyncTimeoutMs)
+ await waitForInitialSync(handles.bindings, 1_000)
+ await makeConcurrentEdits(handles)
+ // Wait for ensureSync
+ await delay(ensureSyncTimeoutMs + 1_000)
+ assertEqualStates(handles)
+ await handles.dispose()
+ })
+
+ test('Concurrent edits settle on equal states (no ensureSync)', async function () {
+ this.timeout(20_000)
+ const handles = await mkHandles(0)
+ await waitForInitialSync(handles.bindings, 1_000)
+ // Ensure both documents are visible:
+ // only `TextEditor.edit`s are expected to converge without ensureSync.
+ await vs.window.showTextDocument(handles.docs[0], { viewColumn: COLUMNS[0], preview: false })
+ await vs.window.showTextDocument(handles.docs[1], { viewColumn: COLUMNS[1], preview: false })
+ await makeConcurrentEdits(handles)
+ await waitForQuiescence(handles.bindings, 3_000)
+ await assertEqualStates(handles)
+ await handles.dispose()
+ })
+})
diff --git a/vscode-workbench/test/extension.test.ts b/vscode-workbench/test/extension.test.ts
deleted file mode 100644
index 7197e15..0000000
--- a/vscode-workbench/test/extension.test.ts
+++ /dev/null
@@ -1,11 +0,0 @@
-import * as assert from 'assert'
-import * as vscode from 'vscode'
-
-suite('Extension Test Suite', () => {
- vscode.window.showInformationMessage('Start all tests.')
-
- test('Sample test', () => {
- assert.strictEqual(-1, [1, 2, 3].indexOf(5))
- assert.strictEqual(-1, [1, 2, 3].indexOf(0))
- })
-})
diff --git a/vscode-workbench/tsconfig.json b/vscode-workbench/tsconfig.json
index 23d772a..96b9bed 100644
--- a/vscode-workbench/tsconfig.json
+++ b/vscode-workbench/tsconfig.json
@@ -1,8 +1,4 @@
{
"extends": "../tsconfig.json",
- "compilerOptions": {
- "noEmit": false,
- "outDir": "out"
- },
"include": ["src/**/*.ts", "test/**/*.ts"]
}