c3faad1730
help break_within to split names at `.`
2023-03-04 12:47:30 +01:00
1c44e861be
fix: search.html for relative roots
2023-01-29 14:07:21 +01:00
3a977a94ca
Fix issues with Search page impelementation
...
- Makes the autocomplete results highlight with up/down arrows.
- Allows you to unselect autocomplete results by using arrow keys.
- Fixed a bug in previous commits where enter did not take you to autocomplete result.
- Return now goes to the search page if no autocomplete result is selected.
- Search results table now properly wraps. (It would be nice to make it wider but I wasn't able to).
- Fixed a bug in the previous commit where docs were not showing, due to failure to copy a modified js file.
2023-01-28 23:00:53 +01:00
033003c6cb
Add a search page to the docs.
...
Now instead of clicking the "Google Site Search"' button, the user has the option
of clicking the "Search" button, which will take them to a results page. Currently,
the results are identical to the autocomplete results, but the number of results
is not limited to 30. In the future, more information and search options could
be added to this page to make a more powerful search.
Fixes #107
2023-01-28 23:00:53 +01:00
f74443a673
style: Lean 4 compiler style in output
2023-01-01 19:51:01 +01:00
f221bbdcff
fix: save the expansion state of the tree again
2022-12-13 20:01:11 +01:00
664a86e08b
fix: minor style improvements
2022-11-06 13:53:23 +01:00
6be2e4dc4e
feat: importedBy via Javascript
2022-07-22 16:56:51 +02:00
2ffff99f90
feat: instances from JSON
2022-07-22 16:15:37 +02:00
0cff3d7cda
fix: Javascript errors in the navbar
2022-07-21 23:01:15 +02:00
80cb92eb94
feat: Use iframe for navbar to move it into the finalize stage
2022-07-21 22:06:26 +02:00
25b1ddb66b
feat: Preparations to split doc-gen build process
2022-07-21 01:40:04 +02:00
12fe918b2d
doc: Output.Template
2022-05-19 21:53:03 +02:00
279df92555
refactor: restructure the modules
2022-05-19 20:41:07 +02:00
41f6eb0835
refactor: use `rawIdent`
2022-05-19 11:20:58 +02:00
06c20ee46f
dynamically change SITE_ROOT since we are relative now
2022-04-07 12:39:32 +02:00
f23556739f
refactor: clean up javascript code
2022-02-22 12:40:14 +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
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
5dc3ab855f
feat: config mathjax like doc-gen
2022-02-18 03:27:00 +08:00
89f5951f2d
feat: add mathjax equation support
2022-02-18 03:10:48 +08:00
c42db4328a
feat: export search.js info
2022-02-13 15:03:49 +01:00
d39b14cf7a
chore: bump toolchain, bye auto pure
2022-02-12 15:09:13 +01:00
2de568d5ca
feat: List of declarations in internal navbar
2022-01-07 17:43:49 +01:00
d5915fcb13
Revert "feat: Fix siteRoot in JS"
...
This reverts commit dcd57e8c5f
2021-12-15 11:25:10 +01:00
dcd57e8c5f
feat: Fix siteRoot in JS
2021-12-15 09:32:21 +01:00
686f111438
chore: Split Output.lean into multiple files
2021-12-15 09:24:49 +01:00
Max Taldykin
Henrik Böving
Jeremy Salwen
Parth Shastri
Sebastian Ullrich
Xubai Wang