diff --git a/src/packages/sync/editor/generic/sorted-patch-list.ts b/src/packages/sync/editor/generic/sorted-patch-list.ts index a92d626f8e..a576746386 100644 --- a/src/packages/sync/editor/generic/sorted-patch-list.ts +++ b/src/packages/sync/editor/generic/sorted-patch-list.ts @@ -37,10 +37,10 @@ export class SortedPatchList extends EventEmitter { this.from_str = from_str; } - public close(): void { + close = (): void => { this.removeAllListeners(); close(this); - } + }; /* Choose the next available time in ms that is congruent to m modulo n. The congruence condition is so that any time @@ -48,11 +48,11 @@ export class SortedPatchList extends EventEmitter { document with themselves -- two different users are guaranteed to not collide. Note: even if there is a collision, it will automatically fix itself very quickly. */ - public next_available_time( + next_available_time = ( time: Date | number, m: number = 0, - n: number = 1 - ): Date { + n: number = 1, + ): Date => { let t: number; if (typeof time === "number") { t = time; @@ -72,9 +72,9 @@ export class SortedPatchList extends EventEmitter { t += n; } return new Date(t); - } + }; - public add(patches: Patch[]): void { + add = (patches: Patch[]): void => { if (patches.length === 0) { // nothing to do return; @@ -125,9 +125,9 @@ export class SortedPatchList extends EventEmitter { this.patches = this.patches.concat(v); this.patches.sort(patch_cmp); } - } + }; - private newest_snapshot_time(): Date { + private newest_snapshot_time = (): Date => { let t0 = 0; let t: string; for (t in this.all_snapshot_times) { @@ -137,7 +137,7 @@ export class SortedPatchList extends EventEmitter { } } return new Date(t0); - } + }; /* value: Return the value of the document at the given (optional) @@ -155,7 +155,7 @@ export class SortedPatchList extends EventEmitter { as a building block to implement undo. We do not assume that without_times is sorted. */ - public value(time?: Date, force?: boolean, without_times?: Date[]): Document { + value = (time?: Date, force?: boolean, without_times?: Date[]): Document => { // oldest time that is skipped: let oldest_without_time: Date | undefined = undefined; // all skipped times. @@ -309,7 +309,7 @@ export class SortedPatchList extends EventEmitter { // files basically be massively broken! console.warn( "WARNING: unable to apply a patch -- skipping it", - err + err, ); } } @@ -338,11 +338,11 @@ export class SortedPatchList extends EventEmitter { */ return value; - } + }; // VERY Slow -- only for consistency checking purposes and debugging. // If snapshots=false, don't use snapshots. - public value_no_cache(time?: Date, snapshots: boolean = true): Document { + value_no_cache = (time?: Date, snapshots: boolean = true): Document => { let value: Document = this.from_str(""); // default in case no snapshots let start: number = 0; const prev_cutoff: Date = this.newest_snapshot_time(); @@ -378,11 +378,11 @@ export class SortedPatchList extends EventEmitter { } } return value; - } + }; // For testing/debugging. Go through the complete patch history and // verify that all snapshots are correct (or not -- in which case say so). - public validate_snapshots(): void { + validate_snapshots = (): void => { if (this.patches.length === 0) { return; } @@ -410,46 +410,46 @@ export class SortedPatchList extends EventEmitter { } i += 1; } - } + }; // integer index of user who made the patch at given point in time. // Throws an exception if there is no patch at that point in time. - public user_id(time): number { + user_id = (time): number => { const x = this.patch(time); if (x == null) { throw Error(`no patch at ${time}`); } return x.user_id; - } + }; // Returns time when patch was sent out, or undefined. This is // ONLY set if the patch was sent at a significantly different // time than when it was created, e.g., due to it being offline. // Throws an exception if there is no patch at that point in time. - public time_sent(time): Date | undefined { + time_sent = (time): Date | undefined => { return this.patch(time).sent; - } + }; // Patch at a given point in time. // Throws an exception if there is no patch at that point in time. - public patch(time): Patch { + patch = (time): Patch => { const p = this.times[time.valueOf()]; if (p == null) { throw Error(`no patch at ${time}`); } return p; - } + }; - public versions(): Date[] { + versions = (): Date[] => { // Compute and cache result,then return it; result gets cleared when new patches added. if (this.versions_cache == null) { this.versions_cache = this.patches.map((x) => x.time); } return this.versions_cache; - } + }; // Show the history of this document; used mainly for debugging purposes. - public show_history({ + show_history = ({ milliseconds, trunc, log, @@ -457,7 +457,7 @@ export class SortedPatchList extends EventEmitter { milliseconds?: boolean; trunc?: number; log?: Function; - } = {}) { + } = {}) => { if (milliseconds === undefined) { milliseconds = false; } @@ -482,7 +482,7 @@ export class SortedPatchList extends EventEmitter { i, x.user_id, tm_show, - trunc_middle(JSON.stringify(x.patch), trunc) + trunc_middle(JSON.stringify(x.patch), trunc), ); if (s === undefined) { s = this.from_str(x.snapshot != null ? x.snapshot : ""); @@ -498,18 +498,18 @@ export class SortedPatchList extends EventEmitter { s = s.apply_patch(x.patch); } else { log( - `prev=${x.prev.valueOf()} is missing, so not applying this patch` + `prev=${x.prev.valueOf()} is missing, so not applying this patch`, ); } } first_time = false; log( x.snapshot ? "(SNAPSHOT) " : " ", - trunc_middle(s.to_str(), trunc).trim() + trunc_middle(s.to_str(), trunc).trim(), ); i += 1; } - } + }; /* This function does not MAKE a snapshot; it just returns the time at which we must plan to make a snapshot. @@ -537,10 +537,10 @@ export class SortedPatchList extends EventEmitter { more need to be made. This isn't maximally efficient, in that several extra snapshots might get made, but maybe that is OK. */ - public time_of_unmade_periodic_snapshot( + time_of_unmade_periodic_snapshot = ( interval: number, - max_size: number - ): Date | undefined { + max_size: number, + ): Date | undefined => { const n = this.patches.length - 1; let cur_size: number = 0; for (let i = n; i >= 0; i--) { @@ -580,11 +580,11 @@ export class SortedPatchList extends EventEmitter { } } } - } + }; // Times of all snapshots in memory on this client; these are // the only ones we need to worry about for offline patches... - public snapshot_times(): Date[] { + snapshot_times = (): Date[] => { const v: Date[] = []; let t: string; for (t in this.all_snapshot_times) { @@ -592,22 +592,72 @@ export class SortedPatchList extends EventEmitter { } v.sort(cmp_Date); return v; - } + }; /* Return the most recent time of a patch, or undefined if there are no patches. */ - public newest_patch_time(): Date | undefined { + newest_patch_time = (): Date | undefined => { if (this.patches.length === 0) { return; } return this.patches[this.patches.length - 1].time; - } + }; - public count(): number { + count = (): number => { return this.patches.length; - } + }; - public export(): Patch[] { + export = (): Patch[] => { return deep_copy(this.patches); - } + }; + + /* + The heads are all timestamps of known patches that are + not pointed to any known patches (via their own heads). + Unlike most things, the set of heads is by definition + information about exatly what is + ** KNOWN BY THIS CLIENT AT THIS POINT IN TIME ** + and is not something that is meant to be + eventually consistent or the same between different client. + The purpose of these heads is to make it possible to + reconstruct exactly what the version of the document looked + like to the client who made a particular patch. + + NOTE: Equal times in Javascript are not equal and also we store + the patches by time with a key a string (ms since epoch, so we + use ms since epoch for heads. + + > new Date(1735049686724) == new Date(1735049686724) + false + + */ + nonHeads = (): Set => { + const nonHeads = new Set(); + if (this.patches.length === 0) { + return nonHeads; + } + for (const patch of this.patches) { + if (patch.heads != null) { + for (const time of patch.heads) { + nonHeads.add(time); + } + } + } + return nonHeads; + }; + + heads = (): number[] => { + if (this.patches.length === 0) { + return []; + } + const nonHeads = this.nonHeads(); + const v: number[] = []; + for (const time in this.times) { + const t = parseInt(time); + if (!nonHeads.has(t)) { + v.push(t); + } + } + return v; + }; } diff --git a/src/packages/sync/editor/generic/sync-doc.ts b/src/packages/sync/editor/generic/sync-doc.ts index 0023765ee6..a4fc13b893 100644 --- a/src/packages/sync/editor/generic/sync-doc.ts +++ b/src/packages/sync/editor/generic/sync-doc.ts @@ -319,7 +319,7 @@ export class SyncDoc extends EventEmitter { until it is (however long, etc.). If this fails, it closes this SyncDoc. */ - private async init(): Promise { + private init = async (): Promise => { this.assert_not_closed("init"); const log = this.dbg("init"); @@ -351,7 +351,7 @@ export class SyncDoc extends EventEmitter { this.set_state("ready"); this.init_watch(); this.emit_change(); // from nothing to something. - } + }; // True if this client is responsible for managing // the state of this document with respect to @@ -1661,6 +1661,8 @@ export class SyncDoc extends EventEmitter { // (optional) timestamp of previous patch sent // from this session prev: null, + // 0 or more heads at point when this patch was made + heads: null, }; if (this.doctype.patch_format != null) { (query as any).format = this.doctype.patch_format; @@ -2040,7 +2042,7 @@ export class SyncDoc extends EventEmitter { await this.patches_table.save(); }); - private next_patch_time(): Date { + private next_patch_time = (): Date => { let time = this.client.server_time(); assertDefined(this.patch_list); const min_time = this.patch_list.newest_patch_time(); @@ -2053,9 +2055,9 @@ export class SyncDoc extends EventEmitter { this.users.length, ); return time; - } + }; - private commit_patch(time: Date, patch: XPatch): void { + private commit_patch = (time: Date, patch: XPatch): void => { this.assert_not_closed("commit_patch"); const obj: any = { // version for database @@ -2063,6 +2065,7 @@ export class SyncDoc extends EventEmitter { time, patch: JSON.stringify(patch), user_id: this.my_user_id, + heads: this.heads(), }; this.my_patches[time.valueOf()] = obj; @@ -2090,13 +2093,16 @@ export class SyncDoc extends EventEmitter { assertDefined(this.patch_list); this.patch_list.add([y]); } - } + }; /* Create and store in the database a snapshot of the state of the string at the given point in time. This should be the time of an existing patch. */ - private async snapshot(time: Date, force: boolean = false): Promise { + private snapshot = async ( + time: Date, + force: boolean = false, + ): Promise => { assertDefined(this.patch_list); const x = this.patch_list.patch(time); if (x == null) { @@ -2198,11 +2204,11 @@ export class SyncDoc extends EventEmitter { last_snapshot: time, }); this.last_snapshot = time; - } + }; // Have a snapshot every this.snapshot_interval patches, except // for the very last interval. - private async snapshot_if_necessary(): Promise { + private snapshot_if_necessary = async (): Promise => { if (this.get_state() !== "ready") return; const dbg = this.dbg("snapshot_if_necessary"); const max_size = Math.floor(1.2 * MAX_FILE_SIZE_MB * 1000000); @@ -2219,7 +2225,7 @@ export class SyncDoc extends EventEmitter { } else { dbg("no need to make a snapshot yet"); } - } + }; /*- x - patch object - time0, time1: optional range of times @@ -2227,12 +2233,12 @@ export class SyncDoc extends EventEmitter { - patch: if given will be used as an actual patch instead of x.patch, which is a JSON string. */ - private process_patch( + private process_patch = ( x: Map, time0?: Date, time1?: Date, patch?: any, - ): Patch | undefined { + ): Patch | undefined => { let t = x.get("time"); if (!is_date(t)) { // who knows what is in the database... @@ -2293,18 +2299,22 @@ export class SyncDoc extends EventEmitter { if (prev != null) { obj.prev = prev; } + const heads = x.get("heads"); + if (heads != null) { + obj.heads = heads.toJS(); + } if (snapshot != null) { obj.snapshot = snapshot; } return obj; - } + }; /* Return all patches with time such that time0 <= time <= time1; If time0 undefined then sets time0 equal to time of last_snapshot. If time1 undefined treated as +oo. */ - private get_patches(time0?: Date, time1?: Date): Patch[] { + private get_patches = (time0?: Date, time1?: Date): Patch[] => { this.assert_table_is_ready("patches"); if (time0 == null) { @@ -2327,7 +2337,7 @@ export class SyncDoc extends EventEmitter { }); v.sort(patch_cmp); return v; - } + }; public has_full_history = (): boolean => { return !this.last_snapshot || this.load_full_history_done; @@ -3337,4 +3347,11 @@ export class SyncDoc extends EventEmitter { newest_patch_time = () => { return this.patch_list?.newest_patch_time(); }; + + heads = () : number[] => { + if (this.patch_list == null) { + throw Error("patch_list not defined"); + } + return this.patch_list?.heads(); + }; } diff --git a/src/packages/sync/editor/generic/types.ts b/src/packages/sync/editor/generic/types.ts index 45907bc099..c913066026 100644 --- a/src/packages/sync/editor/generic/types.ts +++ b/src/packages/sync/editor/generic/types.ts @@ -23,6 +23,7 @@ export interface Patch { sent?: Date; // when patch actually sent, which may be later than when made prev?: Date; // timestamp of previous patch sent from this session size: number; // size of the patch (by defn length of string representation) + heads?: number[]; // heads known by this client when patch was created } export interface Document { diff --git a/src/packages/util/db-schema/syncstring-schema.ts b/src/packages/util/db-schema/syncstring-schema.ts index dbfb013a24..9d4d873214 100644 --- a/src/packages/util/db-schema/syncstring-schema.ts +++ b/src/packages/util/db-schema/syncstring-schema.ts @@ -311,7 +311,12 @@ Table({ }, prev: { type: "timestamp", - desc: "Optional field to indicate patch dependence; if given, don't apply this patch until the patch with timestamp prev has been applied.", + desc: "timestamp of previous patch that this user sent from this session", + }, + heads: { + type: "array", + pg_type: "bigint[]", + desc: "timestamps of heads when this patch was made. It's an array due to merges. Note that bigint (8 bytes) is big enough for this, but integer is NOT.", }, format: { type: "integer", @@ -332,6 +337,7 @@ Table({ snapshot: null, sent: null, prev: null, + heads: null, format: null, }, check_hook(db, obj, account_id, project_id, cb) { @@ -353,6 +359,7 @@ Table({ snapshot: true, sent: true, prev: true, + heads: true, format: true, }, required_fields: {