Commit Graph

170 Commits (0ec492ba98759f629c8e44c35fa8196489d3b977)

Author SHA1 Message Date
Xubai Wang 0ec492ba98 fix: error handling for declaration data 2022-03-14 10:59:25 +08:00
Henrik Böving 5e2e30c4f6
Merge pull request #46 from leanprover/lake
Lake integration
2022-03-06 18:55:29 +01:00
Henrik Böving 9cc4c787e6 feat: lake integration 2022-03-06 18:51:06 +01:00
Henrik Böving 5535616725 chore: Bump toolchain 2022-03-06 16:48:49 +01:00
Henrik Böving 6492f827b7 chore: bump toolchain 2022-02-27 18:01:34 +01:00
Henrik Böving 24b0094574
Merge pull request #45 from xubaiw/better-includestr
Make include_str relative to file
2022-02-26 16:39:38 +01:00
Xubai Wang 5f7d380ab7 refactor: make include_str relative to file 2022-02-26 09:41:25 +08:00
Henrik Böving d63145c304
Merge pull request #42 from leanprover/cli
feat: actual CLI
2022-02-23 22:57:52 +01:00
Henrik Böving 34d2239b68 feat: actual CLI 2022-02-23 22:54:10 +01: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
Henrik Böving 58ce86f93d
Merge pull request #41 from xubaiw/navbar
Navbar
2022-02-23 19:18:22 +01:00
Xubai Wang dca4e42665 fix: filter out nonexist modules 2022-02-23 23:33:34 +08:00
Xubai Wang a50ca857aa fix: wrap navbar overflow 2022-02-23 23:28:15 +08:00
Xubai Wang a5dfba5f1c fix: fix navbar centering 2022-02-23 23:09:10 +08:00
Xubai Wang 2b217ecda0 fix: fix find search 2022-02-23 05:32:37 +08:00
Xubai Wang a18e343829 refactor: change find syntax 2022-02-23 04:26:20 +08:00
Xubai Wang e4ccc5cf50 feat: add browser cache for data
fix search name
2022-02-22 23:20:20 +08:00
Xubai Wang 004977e6e4 refactor: use strict match for find 2022-02-22 15:01:14 +08: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 bc0dd3b48a feat: add src endpoint 2022-02-21 01:38:12 +08:00
Xubai Wang 59707cda58 refactor: use js for find 2022-02-21 01:12:49 +08:00
Xubai Wang 5e93038023 refactor: use js modules 2022-02-21 00:06:15 +08:00
Xubai Wang 842e243241 revert: use bmp extension again 2022-02-20 23:45:31 +08:00
Xubai Wang 73f7906357 refactor: move script into head 2022-02-20 23:42:46 +08:00
Henrik Böving 28bb2abe40
Merge pull request #36 from leanprover/better-equations
Better equations
2022-02-20 16:24:50 +01:00
Xubai Wang a89cf7d7a4 refactor: move siteRoot to separate file 2022-02-20 23:24:08 +08:00
Xubai Wang b9c5109aaf pref: prefetch search data 2022-02-20 23:05:35 +08:00
Xubai Wang 9f13773a7d refactor: use json ext instead of bmp 2022-02-20 22:54:57 +08:00
Henrik Böving a86c384354 fix: Readd equations for instances 2022-02-20 13:52:57 +01: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
Henrik Böving 87a8b8feb0
Merge pull request #33 from xubaiw/docstring
Docstring support
2022-02-20 11:59:44 +01:00
Xubai Wang 2b97d88059 Merge branch 'docstring' of https://github.com/xubaiw/doc-gen4 into docstring 2022-02-20 13:37:03 +08:00
Xubai Wang 2151813fe5 feat: allow intra link in code block 2022-02-20 13:28:48 +08:00
Xubai Wang ad4d77a9c9 fix: change same end maching 2022-02-20 11:43:27 +08:00
Xubai Wang 4c2d67cfca fix: change same end maching 2022-02-20 05:03:44 +08:00
Xubai Wang 794923a997 fix: update Unicode.lean 2022-02-20 04:50:04 +08:00
Xubai Wang 189e5dacdb Merge remote-tracking branch 'upstream/main' into docstring 2022-02-20 03:40:55 +08:00
Xubai Wang 3acfc510b4 fix: no overmatch for intra link 2022-02-20 03:28:03 +08:00
Xubai Wang 5e550c7833 refactor: docstring between basic and extra info
clean up code
2022-02-20 03:14:58 +08:00
Henrik Böving d0714c3aab chore: Don't hard code the path seps in the build dir 2022-02-19 18:15:43 +01:00
Henrik Böving bd9ab34655
Merge pull request #34 from xubaiw/parent-module-nav
fix: add nav link to non leaf node modules
2022-02-18 22:34:57 +01: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 52d087a189 Merge branch 'parent-module-nav' of https://github.com/xubaiw/doc-gen4 into parent-module-nav 2022-02-18 14:13:43 +08:00
Xubai Wang 2f5a95b312 fix: add nav link to non leaf node modules 2022-02-18 14:12:05 +08:00
Xubai Wang 828449ebb4 fix: add nav link to non leaf node modules 2022-02-18 14:03:54 +08:00
Xubai Wang 3687b3466a refactor: clean up docstring module 2022-02-18 12:52:01 +08:00
Xubai Wang d8a5f52c10 fix: fix docstring order 2022-02-18 11:28:44 +08:00
Xubai Wang 0724806fe6 Merge branch 'docstring' of https://github.com/xubaiw/doc-gen4 into docstring 2022-02-18 04:01:34 +08:00