r
/
bookshelf
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

`declaration-data.js` changes up to `9b524d7`.

finite-set-exercises
Joshua Potter 2023-07-26 13:48:54 -06:00
parent c3b579aed1
commit da2cde9af3
1 changed files with 32 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
static/declaration-data.js
View File

@ -24,7 +24,7 @@ export class DeclarationDataCenter {
/** /**
* Used to implement the singleton, in case we need to fetch data mutiple times in the same page. * Used to implement the singleton, in case we need to fetch data mutiple times in the same page.
*/ */
static singleton = null; static requestSingleton = null;
/** /**
* Construct a DeclarationDataCenter with given data. * Construct a DeclarationDataCenter with given data.
@ -41,7 +41,13 @@ export class DeclarationDataCenter {
* @returns {Promise<DeclarationDataCenter>} * @returns {Promise<DeclarationDataCenter>}
*/ */
static async init() { static async init() {
if (!DeclarationDataCenter.singleton) { if (DeclarationDataCenter.requestSingleton === null) {
DeclarationDataCenter.requestSingleton = DeclarationDataCenter.getData();
}
return await DeclarationDataCenter.requestSingleton;
}
static async getData() {
const dataListUrl = new URL( const dataListUrl = new URL(
`${SITE_ROOT}/declarations/declaration-data.bmp`, `${SITE_ROOT}/declarations/declaration-data.bmp`,
window.location window.location
@ -51,17 +57,16 @@ export class DeclarationDataCenter {
const data = await fetchCachedDeclarationData().catch(_e => null); const data = await fetchCachedDeclarationData().catch(_e => null);
if (data) { if (data) {
// if data is defined, use the cached one. // if data is defined, use the cached one.
DeclarationDataCenter.singleton = new DeclarationDataCenter(data); return new DeclarationDataCenter(data);
} else { } else {
// undefined. then fetch the data from the server. // undefined. then fetch the data from the server.
const dataListRes = await fetch(dataListUrl); const dataListRes = await fetch(dataListUrl);
const data = await dataListRes.json(); const data = await dataListRes.json();
await cacheDeclarationData(data); // TODO https://github.com/leanprover/doc-gen4/issues/133
DeclarationDataCenter.singleton = new DeclarationDataCenter(data); // await cacheDeclarationData(data);
return new DeclarationDataCenter(data);
} }
} }
return DeclarationDataCenter.singleton;
}
/** /**
* Search for a declaration. * Search for a declaration.
@ -268,7 +273,12 @@ async function fetchCachedDeclarationData() {
return new Promise((resolve, reject) => { return new Promise((resolve, reject) => {
let transactionRequest = store.get(CACHE_DB_KEY); let transactionRequest = store.get(CACHE_DB_KEY);
transactionRequest.onsuccess = function (event) { transactionRequest.onsuccess = function (event) {
resolve(event.result); // TODO: This API is not thought 100% through. If we have a DB cached
// already it will not even ask the remote for a new one so we end up
// with outdated declaration-data. This has to have some form of cache
// invalidation: https://github.com/leanprover/doc-gen4/issues/133
// resolve(event.target.result);
resolve(undefined);
}; };
transactionRequest.onerror = function (event) { transactionRequest.onerror = function (event) {
reject(new Error(`fail to store declaration data`)); reject(new Error(`fail to store declaration data`));