Commit Graph

443 Commits (main)

Author SHA1 Message Date
Henrik Böving 2e4642e17c chore: port legacy syntax to rawIdent 2022-05-19 17:16:40 +02:00
Henrik Böving 953d9dc304
Merge pull request #52 from Kha/rawIdent
refactor: use `rawIdent`
2022-05-19 11:43:28 +02:00
Sebastian Ullrich 41f6eb0835 refactor: use `rawIdent` 2022-05-19 11:20:58 +02:00
Henrik Böving fc48deaf81
Merge pull request #51 from leanprover/compiler-attrs
More compiler related attributes.
2022-04-19 20:32:56 +02:00
Henrik Böving 24a24d75c7 feat: csimp attribute 2022-04-19 20:28:30 +02:00
Henrik Böving 9a6bf85588 chore: update toolchain 2022-04-19 20:18:28 +02:00
Henrik Böving ea66f7f243 feat: export attribute 2022-04-12 19:11:45 +02:00
Henrik Böving 2128e789ca
Merge pull request #49 from leanprover/ctor-field-docs
Structure field doc strings
2022-04-09 22:34:04 +02:00
Henrik Böving a7c00d95e6 feat: Render doc comments for structure fields 2022-04-09 21:39:34 +02:00
Henrik Böving 89dd2fa46e chore: upgrade compiler version 2022-04-09 19:30:33 +02:00
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