Henrik Böving
|
b22818b971
|
feat: render foundational types info
|
2022-11-22 21:07:59 +01:00 |
|
Henrik Böving
|
ed4cee2eae
|
chore: style, change $ to <|
|
2022-07-23 13:01:25 +02:00 |
|
Henrik Böving
|
5a65c64d4c
|
fix: alignment of navbar
|
2022-07-22 17:18:09 +02:00 |
|
Henrik Böving
|
0cff3d7cda
|
fix: Javascript errors in the navbar
|
2022-07-21 23:01:15 +02:00 |
|
Henrik Böving
|
80cb92eb94
|
feat: Use iframe for navbar to move it into the finalize stage
|
2022-07-21 22:06:26 +02:00 |
|
Henrik Böving
|
25b1ddb66b
|
feat: Preparations to split doc-gen build process
|
2022-07-21 01:40:04 +02:00 |
|
Henrik Böving
|
5b56be76f2
|
chore: Cleanup HTML syntax and pretty printing
|
2022-06-21 20:54:29 +02:00 |
|
Henrik Böving
|
94ce87d11a
|
doc: Output.Navbar
|
2022-05-19 21:49:25 +02:00 |
|
Henrik Böving
|
20e136bb27
|
refactor: centralized methods for internal linking infrastructure
|
2022-05-19 21:49:16 +02:00 |
|
Henrik Böving
|
279df92555
|
refactor: restructure the modules
|
2022-05-19 20:41:07 +02:00 |
|
Henrik Böving
|
2e4642e17c
|
chore: port legacy syntax to rawIdent
|
2022-05-19 17:16:40 +02:00 |
Sebastian Ullrich
|
41f6eb0835
|
refactor: use `rawIdent`
|
2022-05-19 11:20:58 +02:00 |
Xubai Wang
|
dca4e42665
|
fix: filter out nonexist modules
|
2022-02-23 23:33:34 +08:00 |
|
Xubai Wang
|
a5dfba5f1c
|
fix: fix navbar centering
|
2022-02-23 23:09:10 +08:00 |
|
Xubai Wang
|
1ef736c014
|
fix: use flattened Html element
|
2022-02-19 02:07:25 +08:00 |
|
Xubai Wang
|
c31aef8e87
|
fix: remove redundant link to parent module
|
2022-02-19 01:54:20 +08:00 |
|
Xubai Wang
|
2f5a95b312
|
fix: add nav link to non leaf node modules
|
2022-02-18 14:12:05 +08:00 |
|
Henrik Böving
|
d39b14cf7a
|
chore: bump toolchain, bye auto pure
|
2022-02-12 15:09:13 +01:00 |
Gabriel Ebner
|
5ed0a8e99f
|
fix: do not show top-level modules twice in navbar
|
2022-01-20 15:38:48 +01:00 |
|
Gabriel Ebner
|
69b5ee76d3
|
chore: use attribute spreads
|
2022-01-20 15:38:48 +01:00 |
|
Henrik Böving
|
0efbcd1f60
|
feat: Newline free HTML formatting
Some of the HTML elements we are generating are newline sensitive
which requires the HTML to String formatter to optionally omit
additional newlines.
|
2021-12-25 14:04:35 +01:00 |
|
Henrik Böving
|
3c01cf1e68
|
feat: Name linking
|
2021-12-17 17:20:44 +01:00 |
|
Henrik Böving
|
2adf5125c1
|
feat: Fix outputs paths
|
2021-12-15 11:59:13 +01:00 |
|
Henrik Böving
|
686f111438
|
chore: Split Output.lean into multiple files
|
2021-12-15 09:24:49 +01:00 |