dynamically change SITE_ROOT since we are relative now

main
Henrik Böving 2022-04-07 12:39:32 +02:00
parent 00837fd089
commit 06c20ee46f
5 changed files with 5 additions and 10 deletions

View File

@ -118,8 +118,6 @@ def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String
FS.writeFile declarationDataPath json.compress FS.writeFile declarationDataPath json.compress
FS.writeFile (basePath / "declaration-data.timestamp") <| toString (←declarationDataPath.metadata).modified.sec FS.writeFile (basePath / "declaration-data.timestamp") <| toString (←declarationDataPath.metadata).modified.sec
let root := Id.run <| ReaderT.run (getRoot) config
FS.writeFile (basePath / "site-root.js") (siteRootJs.replace "{siteRoot}" root)
FS.writeFile (basePath / "declaration-data.js") declarationDataCenterJs FS.writeFile (basePath / "declaration-data.js") declarationDataCenterJs
FS.writeFile (basePath / "nav.js") navJs FS.writeFile (basePath / "nav.js") navJs
FS.writeFile (basePath / "find" / "find.js") findJs FS.writeFile (basePath / "find" / "find.js") findJs

View File

@ -52,7 +52,6 @@ def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath :=
section Static section Static
def styleCss : String := include_str "../../static/style.css" def styleCss : String := include_str "../../static/style.css"
def siteRootJs : String := include_str "../../static/site-root.js"
def declarationDataCenterJs : String := include_str "../../static/declaration-data.js" def declarationDataCenterJs : String := include_str "../../static/declaration-data.js"
def navJs : String := include_str "../../static/nav.js" def navJs : String := include_str "../../static/nav.js"
def howAboutJs : String := include_str "../../static/how-about.js" def howAboutJs : String := include_str "../../static/how-about.js"

View File

@ -17,7 +17,7 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do
<head> <head>
<title>{title}</title> <title>{title}</title>
<meta charset="UTF-8"/> <meta charset="UTF-8"/>
<meta name="viewport" content="width=device-width, initial-scale=1"/> <meta name="viewport" content="width=device-width, initial-scale=1"/>
@ -29,13 +29,14 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do
<script defer="true" src={s!"{←getRoot}mathjax-config.js"}></script> <script defer="true" src={s!"{←getRoot}mathjax-config.js"}></script>
<script defer="true" src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script> <script defer="true" src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script>
<script defer="true" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script> <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>
<script type="module" src={s!"{←getRoot}nav.js"}></script> <script type="module" src={s!"{←getRoot}nav.js"}></script>
<script type="module" src={s!"{←getRoot}search.js"}></script> <script type="module" src={s!"{←getRoot}search.js"}></script>
<script type="module" src={s!"{←getRoot}how-about.js"}></script> <script type="module" src={s!"{←getRoot}how-about.js"}></script>
</head> </head>
<body> <body>
<input id="nav_toggle" type="checkbox"/> <input id="nav_toggle" type="checkbox"/>
@ -52,7 +53,7 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do
</header> </header>
[site] [site]
{←navbar} {←navbar}
</body> </body>

View File

@ -4,8 +4,6 @@
* Please see {@link DeclarationDataCenter} for more information. * Please see {@link DeclarationDataCenter} for more information.
*/ */
import { SITE_ROOT } from "./site-root.js";
const CACHE_DB_NAME = "declaration-data"; const CACHE_DB_NAME = "declaration-data";
const CACHE_DB_VERSION = 1; const CACHE_DB_VERSION = 1;

View File

@ -15,7 +15,6 @@
* fallback to the `#doc` view. * fallback to the `#doc` view.
*/ */
import { SITE_ROOT } from "../site-root.js";
import { DeclarationDataCenter } from "../declaration-data.js"; import { DeclarationDataCenter } from "../declaration-data.js";
/** /**