Henrik Böving
|
b58b1b315b
|
refactor: finally split upt the process module
|
2022-05-20 00:36:21 +02:00 |
|
Henrik Böving
|
8e70777059
|
chore: copyright header
|
2022-05-19 21:56:43 +02:00 |
|
Henrik Böving
|
12fe918b2d
|
doc: Output.Template
|
2022-05-19 21:53:03 +02:00 |
|
Henrik Böving
|
8e4b7bdb50
|
doc: Output.Structure
|
2022-05-19 21:52:54 +02:00 |
|
Henrik Böving
|
3fd17bd261
|
doc: Output.NotFound
|
2022-05-19 21:49:50 +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
|
e0bf4ad28c
|
doc: Output/Definition
|
2022-05-19 21:07:44 +02:00 |
|
Henrik Böving
|
bdd4a5f612
|
doc: Output.Base
|
2022-05-19 21:05:17 +02:00 |
|
Henrik Böving
|
0b8f7a1397
|
doc: Output top level module
|
2022-05-19 20:54:42 +02:00 |
|
Henrik Böving
|
653c67e9b7
|
doc: SourceLinker
|
2022-05-19 20:52:54 +02:00 |
|
Henrik Böving
|
43f7786523
|
refactor: pull source linker into submodule
|
2022-05-19 20:48:26 +02:00 |
|
Henrik Böving
|
c05a9cf5e5
|
doc: Load
|
2022-05-19 20:45:12 +02:00 |
|
Henrik Böving
|
5fd076530e
|
doc: IncludeStr
|
2022-05-19 20:41:45 +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 |
|
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 |