mirror of
https://github.com/anoma/juvix.git
synced 2024-12-14 17:32:00 +03:00
22027f137c
This PR redefines the `html` command unifying our previous subcommands for the HTML backend. You should use the command in the following way to obtain the same results as before: - `juvix html src.juvix` -> `juvix html src.juvix --only-source` - `juvix dev doc src.juvix` -> `juvix html src.juvix` - Other fixes here include the flag `--non-recursive`, which replaces the previous behavior in that we now generate all the HTML recursively by default. - The flag `--no-print-metadata` is now called `--no-footer` - Also, another change introduced by this PR is asset handling; for example, with our canonical Juvix program, the new output is organized as follows. ``` juvix html HelloWorld.juvix --only-source && tree html/ Copying assets files to test/html/assets Writing HelloWorld.html html/ ├── assets │ ├── css │ │ ├── linuwial.css │ │ ├── source-ayu-light.css │ │ └── source-nord.css │ ├── images │ │ ├── tara-magicien.png │ │ ├── tara-seating.svg │ │ ├── tara-smiling.png │ │ ├── tara-smiling.svg │ │ ├── tara-teaching.png │ │ └── tara-teaching.svg │ └── js │ ├── highlight.js │ └── tex-chtml.js └── HelloWorld.html ├── Stdlib.Data.Bool.html ├── Stdlib.Data.List.html ├── Stdlib.Data.Maybe.html ├── Stdlib.Data.Nat.html ├── Stdlib.Data.Ord.html ├── Stdlib.Data.Product.html ├── Stdlib.Data.String.html ├── Stdlib.Function.html ├── Stdlib.Prelude.html └── Stdlib.System.IO.html ``` In addition, for the vscode-plugin, this PR adds two flags, `--prefix-assets` and `--prefix-url`, for which one provides input to help vscode find resource locations and Juvix files. PS. Make sure to run `make clean` the first time you run `make install` for the first time.
27 lines
567 B
JavaScript
27 lines
567 B
JavaScript
var highlight = function (on) {
|
|
return function () {
|
|
var links = document.getElementsByTagName('a');
|
|
for (var i = 0; i < links.length; i++) {
|
|
var that = links[i];
|
|
|
|
if (this.href != that.href) {
|
|
continue;
|
|
}
|
|
|
|
if (on) {
|
|
that.classList.add("hover-highlight");
|
|
} else {
|
|
that.classList.remove("hover-highlight");
|
|
}
|
|
}
|
|
};
|
|
};
|
|
|
|
window.onload = function () {
|
|
var links = document.getElementsByTagName('a');
|
|
for (var i = 0; i < links.length; i++) {
|
|
links[i].onmouseover = highlight(true);
|
|
links[i].onmouseout = highlight(false);
|
|
}
|
|
};
|