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
Xubai Wang
cce4285c96
fix: intersperse code contents
2022-02-18 04:01:31 +08:00
王虚白
5ce1ce9fe7
Merge branch 'main' into docstring
2022-02-18 03:38:20 +08:00
Xubai Wang
5dc3ab855f
feat: config mathjax like doc-gen
2022-02-18 03:27:00 +08:00
Xubai Wang
9550d1c92e
refactor: use ## for intra doc
2022-02-18 03:26:38 +08:00