diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 21ebb15..7351530 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -80,7 +80,7 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do let link := root ++ s!"semantic/{decl.getName.hash}.xml#" let docLink := Id.run <| ReaderT.run (declNameToLink decl.getName) config let sourceLink := Id.run <| ReaderT.run (getSourceUrl mod.name decl.getDeclarationRange) config - let obj := Json.mkObj [("name", name), ("doc", doc), ("link", link), ("docLink", docLink), ("sourcLink", sourceLink)] + let obj := Json.mkObj [("name", name), ("doc", doc), ("link", link), ("docLink", docLink), ("sourceLink", sourceLink)] declList := declList.push obj let xml := toString <| Id.run <| ReaderT.run (semanticXml decl) config FS.writeFile (basePath / "semantic" / s!"{decl.getName.hash}.xml") xml diff --git a/static/declaration-data.js b/static/declaration-data.js index 2439e4a..cb7a90c 100644 --- a/static/declaration-data.js +++ b/static/declaration-data.js @@ -56,8 +56,7 @@ export class DeclarationDataCenter { const timestamp = await timestampRes.text(); // try to use cache first - let store = await getDeclarationStore(); - const data = await fetchCachedDeclarationData(store, timestamp); + const data = await fetchCachedDeclarationData(timestamp); if (data) { // if data is defined, use the cached one. DeclarationDataCenter.singleton = new DeclarationDataCenter(data); @@ -79,9 +78,7 @@ export class DeclarationDataCenter { }, ]) ); - // get store again in case it's inactive - let store = await getDeclarationStore(); - await cacheDeclarationData(store, timestamp, data); + await cacheDeclarationData(timestamp, data); DeclarationDataCenter.singleton = new DeclarationDataCenter(data); } } @@ -156,7 +153,15 @@ function getMatches(declarations, pattern, maxResults = 30) { err = 3; } if (err !== undefined) { - results.push({ name, err, lowerName, lowerDoc, link, docLink, sourceLink }); + results.push({ + name, + err, + lowerName, + lowerDoc, + link, + docLink, + sourceLink, + }); } } return results.sort(({ err: a }, { err: b }) => a - b).slice(0, maxResults); @@ -166,11 +171,12 @@ function getMatches(declarations, pattern, maxResults = 30) { /** * Get the indexedDB database, automatically initialized. - * @returns {Promise} + * @returns {Promise} */ -function getDeclarationStore() { +async function getDeclarationDatabase() { return new Promise((resolve, reject) => { const request = indexedDB.open(CACHE_DB_NAME, CACHE_DB_VERSION); + request.onerror = function (event) { reject( new Error( @@ -181,38 +187,33 @@ function getDeclarationStore() { request.onupgradeneeded = function (event) { let db = event.target.result; // We only need to store one object, so no key path or increment is needed. - let objectStore = db.createObjectStore("declaration"); - objectStore.transaction.oncomplete = function (event) { - resolve(objectStore); - }; + db.createObjectStore("declaration"); }; request.onsuccess = function (event) { - resolve( - event.target.result - .transaction("declaration", "readwrite") - .objectStore("declaration") - ); + resolve(event.target.result); }; }); } /** * Store data in indexedDB object store. - * @param {IDBObjectStore} store * @param {string} timestamp * @param {Map} data */ -function cacheDeclarationData(store, timestamp, data) { +async function cacheDeclarationData(timestamp, data) { + let db = await getDeclarationDatabase(); + let store = db + .transaction("declaration", "readwrite") + .objectStore("declaration"); return new Promise((resolve, reject) => { let clearRequest = store.clear(); - clearRequest.onsuccess = function (event) { - let addRequest = store.add(data, timestamp); - addRequest.onsuccess = function (event) { - resolve(); - }; - addRequest.onerror = function (event) { - reject(new Error(`fail to store declaration data`)); - }; + let addRequest = store.add(data, timestamp); + + addRequest.onsuccess = function (event) { + resolve(); + }; + addRequest.onerror = function (event) { + reject(new Error(`fail to store declaration data`)); }; clearRequest.onerror = function (event) { reject(new Error("fail to clear object store")); @@ -222,11 +223,14 @@ function cacheDeclarationData(store, timestamp, data) { /** * Retrieve data from indexedDB database. - * @param {IDBObjectStore} store * @param {string} timestamp * @returns {Promise|undefined>} */ -async function fetchCachedDeclarationData(store, timestamp) { +async function fetchCachedDeclarationData(timestamp) { + let db = await getDeclarationDatabase(); + let store = db + .transaction("declaration", "readonly") + .objectStore("declaration"); return new Promise((resolve, reject) => { let transactionRequest = store.get(timestamp); transactionRequest.onsuccess = function (event) { diff --git a/static/find/find.js b/static/find/find.js index 597ed38..4b65f26 100644 --- a/static/find/find.js +++ b/static/find/find.js @@ -40,6 +40,8 @@ const pattern = queryParams.get("pattern") ?? fragmentPaths[1]; // if first fail const strict = (queryParams.get("strict") ?? "true") === "true"; // default to true const view = fragmentPaths[0]; +findAndRedirect(pattern, strict, view); + /** * Find the result and redirect to the result page. * @param {string} pattern the pattern to search for @@ -59,7 +61,6 @@ async function findAndRedirect(pattern, strict, view) { window.location.replace(`${SITE_ROOT}404.html#${pattern ?? ""}`); } else { // success, redirect to doc or source page, or to the semantic rdf. - window.location.replace(isSource ? results[0].sourceLink : results[0].link); if (!view) { window.location.replace(result.link); } else if (view == "doc") {