/** * This module is used for the `/find` endpoint. * * Two basic kinds of search syntax are supported: * * 1. Query-Fragment syntax: `/find?pattern=Nat.add#doc` for documentation and `/find?pattern=Nat.add#src` for source code. * 2. Fragment-Only syntax:`/find/#doc/Nat.add` for documentation and `/find/#src/Nat.add` for source code. * * Though both of them are valid, the first one is highly recommended, and the second one is for compatibility and taste. * * There are some extended usage for the QF syntax. For example, appending `strict=false` to the query part * (`/find?pattern=Nat.add&strict=false#doc`) will allow you to use the fuzzy search, rather than strict match. * Also, the fragment is extensible as well. For now only `#doc` and `#src` are implement, and the plain query without * hash (`/find?pattern=Nat.add`) is used for computer-friendly data (semantic web is great! :P), while all other fragments * fallback to the `#doc` view. */ import { DeclarationDataCenter } from "../declaration-data.js"; function leanFriendlyRegExp(c) { try { return new RegExp("(? p.split(LEAN_FRIENDLY_EQUAL_SEPARATOR)) ?.filter((l) => l.length == 2 && l[0].length > 0) ); const fragmentPaths = fragment?.split(LEAN_FRIENDLY_SLASH_SEPARATOR) ?? []; const encodedPattern = queryParams.get("pattern") ?? fragmentPaths[1]; // if first fail then second, may be undefined const pattern = encodedPattern && decodeURIComponent(encodedPattern); 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 * @param {string} view the view of the find result (`"doc"` or `"src"` for now) */ async function findAndRedirect(pattern, strict, view) { // if no pattern provided, directly redirect to the 404 page if (!pattern) { window.location.replace(`${SITE_ROOT}404.html`); } // search for result try { const dataCenter = await DeclarationDataCenter.init(); let result = (dataCenter.search(pattern, strict) ?? [])[0]; // in case return non array // if no result found, redirect to the 404 page if (!result) { // TODO: better url semantic for 404, current implementation will lead to duplicate search for fuzzy match if not found. window.location.replace(`${SITE_ROOT}404.html#${pattern ?? ""}`); } else { result.docLink = SITE_ROOT + result.docLink; // success, redirect to doc or source page, or to the semantic rdf. if (!view) { window.location.replace(result.link); } else if (view == "doc") { window.location.replace(result.docLink); } else if (view == "src") { const [module, decl] = result.docLink.split("#", 2); window.location.replace(`${module}?jump=src#${decl}`); } else { // fallback to doc page window.location.replace(result.docLink); } } } catch (e) { document.write(`Cannot fetch data, please check your network connection.\n${e}`); } }