diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index ae4d03a..21ebb15 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -10,6 +10,7 @@ import DocGen4.Output.Index import DocGen4.Output.Module import DocGen4.Output.NotFound import DocGen4.Output.Find +import DocGen4.Output.Semantic namespace DocGen4 @@ -69,19 +70,24 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do let notFoundHtml := ReaderT.run notFound config FS.createDirAll basePath FS.createDirAll (basePath / "find") + FS.createDirAll (basePath / "semantic") let mut declList := #[] for (_, mod) in result.moduleInfo.toArray do for decl in filterMapDocInfo mod.members do let name := decl.getName.toString let doc := decl.getDocString.getD "" - let link := Id.run <| ReaderT.run (declNameToLink decl.getName) config - let source := Id.run <| ReaderT.run (getSourceUrl mod.name decl.getDeclarationRange) config - let obj := Json.mkObj [("name", name), ("doc", doc), ("link", link), ("source", source)] + 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)] declList := declList.push obj - + let xml := toString <| Id.run <| ReaderT.run (semanticXml decl) config + FS.writeFile (basePath / "semantic" / s!"{decl.getName.hash}.xml") xml let json := Json.arr declList + FS.writeFile (basePath / "semantic" / "docgen4.xml") <| toString <| Id.run <| ReaderT.run schemaXml config + FS.writeFile (basePath / "index.html") indexHtml.toString FS.writeFile (basePath / "404.html") notFoundHtml.toString FS.writeFile (basePath / "find" / "index.html") findHtml.toString diff --git a/DocGen4/Output/Semantic.lean b/DocGen4/Output/Semantic.lean new file mode 100644 index 0000000..7b22cdf --- /dev/null +++ b/DocGen4/Output/Semantic.lean @@ -0,0 +1,58 @@ +import DocGen4.Output.Template +import DocGen4.Output.DocString +import Lean.Data.Xml + +open Lean Xml + +namespace DocGen4 +namespace Output + +instance : ToString $ Array Element where + toString xs := xs.map toString |>.foldl String.append "" + +instance : Coe Element Content where + coe e := Content.Element e + +-- TODO: syntax metaprogramming and basic semantic data + +def semanticXml (i : DocInfo) : HtmlM $ Array Element := do + pure #[ + Element.Element + "rdf:RDF" + (Std.RBMap.fromList [ + ("xmlns:rdf", "http://www.w3.org/1999/02/22-rdf-syntax-ns#"), + ("xmlns:docgen4", s!"{←getRoot}semactic/docgen4.xml#") + ] _) + #[ + Element.Element + "rdf:Description" + (Std.RBMap.fromList [ + ("rdf:about", s!"{←getRoot}semactic/{i.getName.hash}.xml#") + ] _) + #[] + ] + ] + +def schemaXml : HtmlM $ Array Element := do + pure #[ + Element.Element + "rdf:RDF" + (Std.RBMap.fromList [ + ("xmlns:rdf", "http://www.w3.org/1999/02/22-rdf-syntax-ns#"), + ("xmlns:docgen4", s!"{←getRoot}semactic/docgen4.xml#") + ] _) + #[ + Element.Element + "docgen4:hasInstance" + Std.RBMap.empty + #[ + Element.Element + "rdfs:type" + Std.RBMap.empty + #[Content.Character "rdf:Property"] + ] + ] + ] + +end Output +end DocGen4 diff --git a/static/declaration-data.js b/static/declaration-data.js index 0cdc869..2439e4a 100644 --- a/static/declaration-data.js +++ b/static/declaration-data.js @@ -67,13 +67,14 @@ export class DeclarationDataCenter { const dataJson = await dataRes.json(); // the data is a map of name (original case) to declaration data. const data = new Map( - dataJson.map(({ name, doc, link, source: sourceLink }) => [ + dataJson.map(({ name, doc, link, docLink, sourceLink }) => [ name, { name, lowerName: name.toLowerCase(), lowerDoc: doc.toLowerCase(), link, + docLink, sourceLink, }, ]) @@ -91,7 +92,7 @@ export class DeclarationDataCenter { * Search for a declaration. * @returns {Array} */ - search(pattern, strict = false) { + search(pattern, strict = true) { if (!pattern) { return []; } @@ -142,6 +143,7 @@ function getMatches(declarations, pattern, maxResults = 30) { lowerName, lowerDoc, link, + docLink, sourceLink, } of declarations.values()) { let err = matchCaseSensitive(name, lowerName, patNoSpaces); @@ -154,7 +156,7 @@ function getMatches(declarations, pattern, maxResults = 30) { err = 3; } if (err !== undefined) { - results.push({ name, err, lowerName, lowerDoc, link, sourceLink }); + results.push({ name, err, lowerName, lowerDoc, link, docLink, sourceLink }); } } return results.sort(({ err: a }, { err: b }) => a - b).slice(0, maxResults); diff --git a/static/find/find.js b/static/find/find.js index 75b5507..597ed38 100644 --- a/static/find/find.js +++ b/static/find/find.js @@ -1,26 +1,74 @@ /** * 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 { SITE_ROOT } from "../site-root.js"; import { DeclarationDataCenter } from "../declaration-data.js"; -async function findRedirect(pattern, isSource) { +/** + * We don't use browser's default hash and searchParams in case Lean declaration name + * can be like `«#»`, rather we manually handle the `window.location.href` with regex. + */ +const LEAN_FRIENDLY_URL_REGEX = /^[^?#]+(?:\?((?:[^«#»]|«.*»)*))?(?:#(.*))?$/; +const LEAN_FRIENDLY_AND_SEPARATOR = /(? p.split(LEAN_FRIENDLY_EQUAL_SEPARATOR)) + ?.filter((l) => l.length == 2 && l[0].length > 0) +); +const fragmentPaths = fragment?.split(LEAN_FRIENDLY_SLASH_SEPARATOR) ?? []; + +const pattern = queryParams.get("pattern") ?? fragmentPaths[1]; // if first fail then second, may be undefined +const strict = (queryParams.get("strict") ?? "true") === "true"; // default to true +const view = fragmentPaths[0]; + +/** + * 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 const dataCenter = await DeclarationDataCenter.init(); - let results = dataCenter.search(pattern, true); - if (results.length == 0) { - // if there is no exact match, redirect to 404 page to use fuzzy match + 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 { - // redirect to doc or source page. + // 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") { + window.location.replace(result.docLink); + } else if (view == "src") { + window.location.replace(result.sourceLink); + } else { + // fallback to doc page + window.location.replace(result.docLink); + } } -} - -let hash = window.location.hash.replace("#", ""); - -if (hash.endsWith("/src")) { - findRedirect(hash.replace("/src", ""), true); -} else { - findRedirect(hash, false); -} +} \ No newline at end of file diff --git a/static/how-about.js b/static/how-about.js index cb9832b..5c03ffd 100644 --- a/static/how-about.js +++ b/static/how-about.js @@ -20,14 +20,14 @@ if (HOW_ABOUT) { if (pattern) { HOW_ABOUT.innerText = "Please wait a second. I'll try to help you."; DeclarationDataCenter.init().then((dataCenter) => { - let results = dataCenter.search(pattern); + let results = dataCenter.search(pattern, false); if (results.length > 0) { HOW_ABOUT.innerText = "How about one of these instead:"; const ul = HOW_ABOUT.appendChild(document.createElement("ul")); - for (const { name, link } of results) { + for (const { name, docLink } of results) { const li = ul.appendChild(document.createElement("li")); const a = li.appendChild(document.createElement("a")); - a.href = link; + a.href = docLink; a.appendChild(document.createElement("code")).innerText = name; } } else { diff --git a/static/search.js b/static/search.js index d5e2fb6..1df8690 100644 --- a/static/search.js +++ b/static/search.js @@ -87,18 +87,18 @@ SEARCH_INPUT.addEventListener("input", async (ev) => { // searching sr.setAttribute("state", "loading"); const dataCenter = await DeclarationDataCenter.init(); - const result = dataCenter.search(text); + const result = dataCenter.search(text, false); // in case user has updated the input. if (ev.target.value != text) return; // update search results removeAllChildren(sr); - for (const { name, link } of result) { + for (const { name, docLink } of result) { const d = sr.appendChild(document.createElement("a")); d.innerText = name; d.title = name; - d.href = link; + d.href = docLink; } sr.setAttribute("state", "done"); });