f23556739f
refactor: clean up javascript code
2022-02-22 12:40:14 +08:00
9e867f5151
refactor: make site-root an actual file
2022-02-21 23:29:23 +08:00
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
bc0dd3b48a
feat: add src endpoint
2022-02-21 01:38:12 +08:00
59707cda58
refactor: use js for find
2022-02-21 01:12:49 +08:00
5e93038023
refactor: use js modules
2022-02-21 00:06:15 +08:00
842e243241
revert: use bmp extension again
2022-02-20 23:45:31 +08:00
73f7906357
refactor: move script into head
2022-02-20 23:42:46 +08:00
28bb2abe40
Merge pull request #36 from leanprover/better-equations
...
Better equations
2022-02-20 16:24:50 +01:00
a89cf7d7a4
refactor: move siteRoot to separate file
2022-02-20 23:24:08 +08:00
b9c5109aaf
pref: prefetch search data
2022-02-20 23:05:35 +08:00
9f13773a7d
refactor: use json ext instead of bmp
2022-02-20 22:54:57 +08:00
a86c384354
fix: Readd equations for instances
2022-02-20 13:52:57 +01:00
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
87a8b8feb0
Merge pull request #33 from xubaiw/docstring
...
Docstring support
2022-02-20 11:59:44 +01:00
2b97d88059
Merge branch 'docstring' of https://github.com/xubaiw/doc-gen4 into docstring
2022-02-20 13:37:03 +08:00
2151813fe5
feat: allow intra link in code block
2022-02-20 13:28:48 +08:00
ad4d77a9c9
fix: change same end maching
2022-02-20 11:43:27 +08:00
4c2d67cfca
fix: change same end maching
2022-02-20 05:03:44 +08:00
794923a997
fix: update Unicode.lean
2022-02-20 04:50:04 +08:00
189e5dacdb
Merge remote-tracking branch 'upstream/main' into docstring
2022-02-20 03:40:55 +08:00
3acfc510b4
fix: no overmatch for intra link
2022-02-20 03:28:03 +08:00
5e550c7833
refactor: docstring between basic and extra info
...
clean up code
2022-02-20 03:14:58 +08:00
d0714c3aab
chore: Don't hard code the path seps in the build dir
2022-02-19 18:15:43 +01:00
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
1ef736c014
fix: use flattened Html element
2022-02-19 02:07:25 +08:00
c31aef8e87
fix: remove redundant link to parent module
2022-02-19 01:54:20 +08:00
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
2f5a95b312
fix: add nav link to non leaf node modules
2022-02-18 14:12:05 +08:00
828449ebb4
fix: add nav link to non leaf node modules
2022-02-18 14:03:54 +08:00
3687b3466a
refactor: clean up docstring module
2022-02-18 12:52:01 +08:00
d8a5f52c10
fix: fix docstring order
2022-02-18 11:28:44 +08:00
0724806fe6
Merge branch 'docstring' of https://github.com/xubaiw/doc-gen4 into docstring
2022-02-18 04:01:34 +08:00
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
5dc3ab855f
feat: config mathjax like doc-gen
2022-02-18 03:27:00 +08:00
9550d1c92e
refactor: use ## for intra doc
2022-02-18 03:26:38 +08:00
89f5951f2d
feat: add mathjax equation support
2022-02-18 03:10:48 +08:00
2dac93d360
fix: fix noncomputable
...
Also address the changes made to module doc until doc strings are implemented.
2022-02-17 18:59:42 +01:00
0b9a9f0bdc
fix: remove intra link in code block
2022-02-18 01:39:02 +08:00
11bb2af57a
feat: add auto link
2022-02-18 00:46:02 +08:00
97ddf05ab6
fix: add root to relative href
2022-02-17 21:26:02 +08:00
1729f4aa71
fix: fix docstring heading id
2022-02-17 15:26:17 +08:00
5790172eab
fix: doc string for all DocInfo
2022-02-17 13:53:29 +08:00
b7c6a98969
refactor: separate docstring code
2022-02-17 13:47:38 +08:00
5679be6bbc
chore: bump lean version
...
update cmark version
2022-02-17 08:54:06 +08:00
d3ce268d63
feat: mod doc heading attributes
2022-02-17 08:16:02 +08:00
385a38a003
feat: basic mod doc without attributes
2022-02-17 08:16:02 +08:00
8da2e2a63d
feat: basic docstring support
2022-02-17 08:16:02 +08:00
28dfc14530
fix: arity in the extern attribute
2022-02-16 21:24:42 +01:00
Xubai Wang
Siddharth Bhat
Henrik Böving
王虚白