Xubai Wang
5f7d380ab7
refactor: make include_str relative to file
2022-02-26 09:41:25 +08:00
Henrik Böving
9dd5e316c1
Merge pull request #38 from xubaiw/win-find
...
Windows find support among other things.
2022-02-23 19:44:47 +01:00
Xubai Wang
f23556739f
refactor: clean up javascript code
2022-02-22 12:40:14 +08:00
Xubai Wang
9e867f5151
refactor: make site-root an actual file
2022-02-21 23:29:23 +08:00
Xubai Wang
59707cda58
refactor: use js for find
2022-02-21 01:12:49 +08:00
Henrik Böving
b87c1cc1de
feat: Better equation Handling
...
The equation content is now escaped, furthermore there is a limit
for the length of an equation so we don't just fill everything with
uselessly big equations nobody can read anyways.
2022-02-20 13:45:18 +01:00
Xubai Wang
5dc3ab855f
feat: config mathjax like doc-gen
2022-02-18 03:27:00 +08:00
Henrik Böving
4b9b7d77d5
chore: Update doc-gen search js
2022-02-13 14:25:37 +01:00
Henrik Böving
d39b14cf7a
chore: bump toolchain, bye auto pure
2022-02-12 15:09:13 +01:00
Henrik Böving
735bfa35a7
chore: update compiler version
2022-01-15 15:35:52 +01:00
Henrik Böving
f7f8138e09
feat: basic source links
2022-01-14 13:36:41 +01:00
Henrik Böving
f71b2ee8b9
chore: Remove obsolete TODOs
2022-01-06 02:05:23 +01:00
Henrik Böving
3adb8e71d1
feat: Show inductive constructors properly
...
Closes : #2
2022-01-03 18:22:12 +01:00
Henrik Böving
3c01cf1e68
feat: Name linking
2021-12-17 17:20:44 +01:00
Henrik Böving
dc5c2ab92a
chore: Add an HtmlT if we need more monads later on
2021-12-17 15:59:04 +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