fix: race condition in declaration-data.js

leanprover · Jul 20, 2023 · 5ce54e8 · 5ce54e8
1 parent 9af4c72
commit 5ce54e8
Showing 1 changed file with 25 additions and 17 deletions.
diff --git a/static/declaration-data.js b/static/declaration-data.js
@@ -25,6 +25,7 @@ export class DeclarationDataCenter {
    * 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.
@@ -41,28 +42,35 @@ export class DeclarationDataCenter {
    * @returns {Promise<DeclarationDataCenter>}
    */
   static async init() {
-    if (!DeclarationDataCenter.singleton) {
-      const dataListUrl = new URL(
-        `${SITE_ROOT}/declarations/declaration-data.bmp`,
-        window.location
-      );
-
-      // try to use cache first
-      const data = await fetchCachedDeclarationData().catch(_e => null);
-      if (data) {
-        // if data is defined, use the cached one.
-        DeclarationDataCenter.singleton = new DeclarationDataCenter(data);
-      } else {
-        // undefined. then fetch the data from the server.
-        const dataListRes = await fetch(dataListUrl);
-        const data = await dataListRes.json();
-        await cacheDeclarationData(data);
-        DeclarationDataCenter.singleton = new DeclarationDataCenter(data);
+    if (DeclarationDataCenter.singleton === null) {
+      if (DeclarationDataCenter.requestSingleton === null) {
+        DeclarationDataCenter.requestSingleton = DeclarationDataCenter.getData();
       }
+      await DeclarationDataCenter.requestSingleton;
     }
     return DeclarationDataCenter.singleton;
   }
 
+  static async getData() {
+    const dataListUrl = new URL(
+      `${SITE_ROOT}/declarations/declaration-data.bmp`,
+      window.location
+    );
+
+    // try to use cache first
+    const data = await fetchCachedDeclarationData().catch(_e => null);
+    if (data) {
+      // if data is defined, use the cached one.
+      DeclarationDataCenter.singleton = new DeclarationDataCenter(data);
+    } else {
+      // undefined. then fetch the data from the server.
+      const dataListRes = await fetch(dataListUrl);
+      const data = await dataListRes.json();
+      await cacheDeclarationData(data);
+      DeclarationDataCenter.singleton = new DeclarationDataCenter(data);
+    }
+  }
+
   /**
    * Search for a declaration.
    * @returns {Array<any>}