CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutSign UpSign In
sagemathinc

Real-time collaboration for Jupyter Notebooks, Linux Terminals, LaTeX, VS Code, R IDE, and more,
all in one place.

GitHub Repository: sagemathinc/cocalc
Path: blob/master/src/packages/sync/editor/generic/patch-value-cache.ts
Views: 687
1
/*
2
* This file is part of CoCalc: Copyright © 2020 Sagemath, Inc.
3
* License: MS-RSL – see LICENSE.md for details
4
*/
5
6
/*
7
The PatchValueCache is used to cache values returned
8
by SortedPatchList.value. Caching is critical, since otherwise
9
the client may have to apply hundreds of patches after ever
10
few keystrokes, which would make CoCalc unusable. Also, the
11
history browser is very painful to use without caching.
12
*/
13
14
import { cmp_Date, keys, cmp, len } from "@cocalc/util/misc";
15
import { Document } from "./types";
16
17
export interface Entry {
18
time: Date;
19
value: Document;
20
start: number;
21
last_used: Date;
22
}
23
24
export class PatchValueCache {
25
// keys in the cache are integers converted to strings.
26
private cache: { [time: string]: Entry } = {};
27
28
// Remove everything from the value cache that has timestamp >= time.
29
// If time not defined, removes everything, thus emptying the cache.
30
public invalidate(time: Date): void {
31
const time0: number = time.valueOf();
32
for (const time in this.cache) {
33
if (parseInt(time) >= time0) {
34
delete this.cache[time];
35
}
36
}
37
}
38
39
// Ensure the value cache doesn't have too many entries in it by
40
// removing all but n of the ones that have not been accessed recently.
41
public prune(n: number): void {
42
if (this.size() <= n) {
43
// nothing to do
44
return;
45
}
46
const v: { time: string; last_used: Date }[] = [];
47
for (const time in this.cache) {
48
const x = this.cache[time];
49
if (x != null) {
50
v.push({ time, last_used: x.last_used });
51
}
52
}
53
v.sort((a, b) => cmp_Date(a.last_used, b.last_used));
54
// Delete oldest n entries.
55
for (const x of v.slice(0, v.length - n)) {
56
delete this.cache[x.time];
57
}
58
}
59
60
// Include the given value at the given point in time, which should be
61
// the output of this.value(time), and should involve applying all patches
62
// up to this.patches[start-1].
63
public include(time: Date, value: Document, start: number) {
64
this.cache[`${time.valueOf()}`] = {
65
time,
66
value,
67
start,
68
last_used: new Date(),
69
};
70
}
71
72
private keys(): number[] {
73
return keys(this.cache).map((x) => parseInt(x));
74
}
75
76
/* Return the newest value x with x.time <= time in the cache as an object
77
78
x={time:time, value:value, start:start},
79
80
where this.value(time) is the given value, and it was obtained
81
by applying the elements of this.patches up to this.patches[start-1]
82
Return undefined if there are no cached values.
83
If time is undefined, returns the newest value in the cache.
84
If strict is true, returns newest value at time strictly older than time
85
*/
86
public newest_value_at_most(
87
time?: Date,
88
strict: boolean = false
89
): Entry | undefined {
90
const v: number[] = this.keys();
91
if (v.length === 0) {
92
return;
93
}
94
v.sort(cmp);
95
v.reverse();
96
if (time == null) {
97
return this.get(v[0]);
98
}
99
const time0 = time.valueOf();
100
for (const t of v) {
101
if ((!strict && t <= time0) || (strict && t < time0)) {
102
return this.get(t);
103
}
104
}
105
}
106
107
/* Return cached entry corresponding to the given point in time.
108
Here time must be either a new Date() object, or a number (ms since epoch).
109
If there is nothing in the cache for the given time, returns undefined.
110
** YOU BETTER NOT mutate the returned value! ** It's not a copy!!
111
*/
112
public get(time: Date | number): Entry | undefined {
113
if (typeof time !== "number") {
114
// also allow dates
115
time = time.valueOf();
116
}
117
const x = this.cache[time];
118
if (x == null) {
119
return;
120
}
121
x.last_used = new Date(); // this is only for the client cache, so fine to use browser's clock
122
return x;
123
}
124
125
public oldest_time(): Date | undefined {
126
const v = this.keys();
127
if (v.length === 0) {
128
return;
129
}
130
v.sort(cmp);
131
return new Date(v[0]);
132
}
133
134
// Number of cached values
135
public size(): number {
136
return len(this.cache);
137
}
138
}
139
140