Commit Graph

283 Commits (4a7c5e214ad15d7099e6b2d6315992e331b149e0)

Author SHA1 Message Date
Henrik Böving 211ade7828 feat: doc strings in ctors and structure fields 2022-04-09 17:27:06 +02:00
Henrik Böving fa2f2b8e05
Merge pull request #48 from leanprover/fix-search
Fix search
2022-04-07 13:20:31 +02:00
Henrik Böving 3ac6ddd1ab fix: port the SITE_ROOT fix to find.js 2022-04-07 13:14:01 +02:00
Henrik Böving 67402506c7 fix: links in search 2022-04-07 12:44:33 +02:00
Henrik Böving 06c20ee46f dynamically change SITE_ROOT since we are relative now 2022-04-07 12:39:32 +02:00
Henrik Böving 00837fd089
Merge pull request #39 from bollu/feb-21-relative-paths-manual-depth
Add support for relative paths
2022-04-07 08:29:01 +02:00
Siddharth Bhat 4bc149a1fb Fix diff nits 2022-04-07 00:53:06 +01:00
Siddharth Bhat 10ed2d489d update README 2022-04-07 00:49:05 +01:00
Siddharth Bhat 9570f25312 cleanup code 2022-04-07 00:48:12 +01:00
Siddharth Bhat f5b9e02766 modify deploy_docs to not need relative path 2022-04-07 00:44:49 +01:00
Siddharth Bhat 9eec1cf1ad URLs now work; Data fetching does not? 2022-04-07 00:31:27 +01:00
Henrik Böving 45374eeced
Merge pull request #47 from xubaiw/brave-indexeddb
Add error handling for declaration data
2022-03-14 18:58:03 +01:00
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
Siddharth Bhat 91891fc4fd Generate relative paths for documentation.
We keep track of the current nesting depth in our Context,
and use this to generate the correct relative path to the root.
2022-02-21 10:14:15 +00: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