feat: importedBy via Javascript
Henrik Böving
parent
2ffff99f90
commit
6be2e4dc4e
|
|
@ -1,3 +1,3 @@
|
|||
/build
|
||||
/lean_packages
|
||||
/lean_packages/*
|
||||
!/lean_packages/manifest.json
|
||||
|
|
|
|||
|
|
@ -126,12 +126,13 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
|
|||
let mut allDecls : List (String × Json) := []
|
||||
let mut allInstances : HashMap String (Array String) := .empty
|
||||
let mut importedBy : HashMap String (Array String) := .empty
|
||||
let mut allModules : List (String × Json) := []
|
||||
for entry in ←System.FilePath.readDir declarationsBasePath do
|
||||
if entry.fileName.startsWith "declaration-data-" && entry.fileName.endsWith ".bmp" then
|
||||
IO.println s!"Processing: {entry.fileName}"
|
||||
let fileContent ← FS.readFile entry.path
|
||||
let .ok jsonContent := Json.parse fileContent | unreachable!
|
||||
let .ok (module : JsonModule) := fromJson? jsonContent | unreachable!
|
||||
allModules := (module.name, Json.str <| moduleNameToLink module.name |>.run baseConfig) :: allModules
|
||||
allDecls := (module.declarations.map (λ d => (d.name, toJson d))) ++ allDecls
|
||||
for inst in module.instances do
|
||||
let mut insts := allInstances.findD inst.className #[]
|
||||
|
|
@ -147,7 +148,8 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
|
|||
let finalJson := Json.mkObj [
|
||||
("declarations", Json.mkObj allDecls),
|
||||
("instances", Json.mkObj postProcessInstances),
|
||||
("importedBy", Json.mkObj postProcessImportedBy)
|
||||
("importedBy", Json.mkObj postProcessImportedBy),
|
||||
("modules", Json.mkObj allModules)
|
||||
]
|
||||
-- The root JSON for find
|
||||
FS.writeFile (declarationsBasePath / "declaration-data.bmp") finalJson.compress
|
||||
|
|
|
|||
|
|
@ -195,7 +195,7 @@ def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
|
|||
</details>
|
||||
<details>
|
||||
<summary>Imported by</summary>
|
||||
<ul id={s!"imported-by-{moduleName}"}> </ul>
|
||||
<ul id={s!"imported-by-{moduleName}"} class="imported-by-list"> </ul>
|
||||
</details>
|
||||
</div>
|
||||
[members.map declarationToNavLink]
|
||||
|
|
|
|||
|
|
@ -15,6 +15,11 @@ open scoped DocGen4.Jsx
|
|||
The HTML template used for all pages.
|
||||
-/
|
||||
def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := do
|
||||
let moduleConstant :=
|
||||
if let some module := (←getCurrentName) then
|
||||
#[<script>{s!"const MODULE_NAME={String.quote module.toString};"}</script>]
|
||||
else
|
||||
#[]
|
||||
pure
|
||||
<html lang="en">
|
||||
<head>
|
||||
|
|
@ -26,6 +31,7 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d
|
|||
<script defer="true" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
|
||||
|
||||
<script>{s!"const SITE_ROOT={String.quote (←getRoot)};"}</script>
|
||||
[moduleConstant]
|
||||
<script type="module" src={s!"{←getRoot}nav.js"}></script>
|
||||
<script type="module" src={s!"{←getRoot}search.js"}></script>
|
||||
<script type="module" src={s!"{←getRoot}how-about.js"}></script>
|
||||
|
|
|
|||
|
|
@ -0,0 +1,20 @@
|
|||
{"version": 1,
|
||||
"packages":
|
||||
[{"url": "https://github.com/mhuisi/lean4-cli",
|
||||
"rev": "112b35fc348a4a18d2111ac2c6586163330b4941",
|
||||
"name": "Cli"},
|
||||
{"url": "https://github.com/hargonix/LeanInk",
|
||||
"rev": "cb529041f71a4ea8348628a8c723326e3e4bdecc",
|
||||
"name": "leanInk"},
|
||||
{"url": "https://github.com/xubaiw/Unicode.lean",
|
||||
"rev": "1fb004da96aa1d1e98535951e100439a60f5b7f0",
|
||||
"name": "Unicode"},
|
||||
{"url": "https://github.com/leanprover-community/mathlib4.git",
|
||||
"rev": "ecd37441047e490ff2ad339e16f45bb8b58591bd",
|
||||
"name": "mathlib"},
|
||||
{"url": "https://github.com/leanprover/lake",
|
||||
"rev": "a7bc6addee9fc07c0ee43d0dcb537faa41844217",
|
||||
"name": "lake"},
|
||||
{"url": "https://github.com/xubaiw/CMark.lean",
|
||||
"rev": "8f17d13d3046c517f7f02062918d81bc69e45cce",
|
||||
"name": "CMark"}]}
|
||||
|
|
@ -99,6 +99,22 @@ export class DeclarationDataCenter {
|
|||
declNameToLink(declName) {
|
||||
return this.declarationData.declarations[declName].docLink;
|
||||
}
|
||||
|
||||
/**
|
||||
* Find all modules that imported the given one.
|
||||
* @returns {Array<String>}
|
||||
*/
|
||||
moduleImportedBy(moduleName) {
|
||||
return this.declarationData.importedBy[moduleName];
|
||||
}
|
||||
|
||||
/**
|
||||
* Analogous to Lean moduleNameToLink
|
||||
* @returns {String}
|
||||
*/
|
||||
moduleNameToLink(moduleName) {
|
||||
return this.declarationData.modules[moduleName];
|
||||
}
|
||||
}
|
||||
|
||||
function isSeparater(char) {
|
||||
|
|
|
|||
|
|
@ -0,0 +1,19 @@
|
|||
import { DeclarationDataCenter } from "./declaration-data.js";
|
||||
|
||||
fillImportedBy();
|
||||
|
||||
async function fillImportedBy() {
|
||||
if (!MODULE_NAME) {
|
||||
return;
|
||||
}
|
||||
const dataCenter = await DeclarationDataCenter.init();
|
||||
const moduleName = MODULE_NAME;
|
||||
const importedByList = document.querySelector(".imported-by-list");
|
||||
const importedBy = dataCenter.moduleImportedBy(moduleName);
|
||||
var innerHTML = "";
|
||||
for(var module of importedBy) {
|
||||
const moduleLink = dataCenter.moduleNameToLink(module);
|
||||
innerHTML += `<li><a href="${SITE_ROOT}${moduleLink}">${module}</a></li>`
|
||||
}
|
||||
importedByList.innerHTML = innerHTML;
|
||||
}
|
||||
|
|
@ -11,7 +11,6 @@ async function annotateInstances() {
|
|||
const instances = dataCenter.instancesForClass(className);
|
||||
var innerHTML = "";
|
||||
for(var instance of instances) {
|
||||
// TODO: probably fix site root
|
||||
const instanceLink = dataCenter.declNameToLink(instance);
|
||||
innerHTML += `<li><a href="${SITE_ROOT}${instanceLink}">${instance}</a></li>`
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue