Commit Graph

178 Commits (3a9cfabe5818692ce2b42214f0e9113263d00743)

Author SHA1 Message Date
Henrik Böving 649e7791fa feat: Respect srcDir configuration in lake 2023-09-27 09:52:22 +02:00
Henrik Böving e1bd706c91 ux: better git error reporting 2023-09-26 23:18:31 +02:00
Mario Carneiro 96870507c5 feat: add jump-src.js for #src links 2023-09-21 11:38:22 +02:00
Alex J. Best 924be4c7d8 feat: expand the current file in the navbar 2023-09-18 23:55:19 +02:00
Henrik Böving 7e89b462f0 chore: update toolchain 2023-09-18 22:08:46 +02:00
Ruben Van de Velde 19568c0659 feat: autolink references to files 2023-09-16 14:37:22 +02:00
Henrik Böving f9b5a2903a fix: header-data.bmp 2023-09-15 00:39:28 +02:00
Henrik f7307953d8 fix: sort expression printing 2023-09-10 14:44:14 +02:00
Henrik 08de0ad10c feat: reduce JSON data size 2023-09-10 12:39:49 +02:00
Henrik b0319462f1 feat: print nameless instances properly 2023-09-09 23:56:21 +02:00
Henrik 3c80369cca Merge remote-tracking branch 'alexjbest/only-linkify-lean' into only-linkify-lean 2023-09-09 23:26:00 +02:00
tydeu 0b52010291 fix: source links for Lake 2023-08-30 19:01:03 +02:00
Henrik d805539b34 chore: update toolchain 2023-08-18 11:07:52 +02:00
Eric Wieser d3d67c1d92 Do the same for inductives 2023-08-18 11:00:32 +02:00
Eric Wieser e5ff71991d Put field docstrings after the field 2023-08-18 11:00:32 +02:00
Henrik 718b182a31 feat: more declaration data as JSON 2023-08-06 15:36:43 +02:00
Henrik e09280bb3c feat: order instances and make them unique in their listing 2023-07-31 20:42:30 +02:00
Calvin Lee 75d06a8153 hide color-changer if javascript is disabled 2023-06-09 23:39:59 +02:00
Calvin Lee cc552ed570 add colorscheme toggle 2023-06-09 23:39:59 +02:00
Alex J. Best 306959b921 feat: list instances for defs also 2023-05-24 01:17:44 +02:00
Henrik cf86cb4815 feat: attempt to source link directory dependencies 2023-04-24 00:18:29 +02:00
Henrik Böving b9421b9a12 fix: Use Z(separator) instead of S(ymbol) category
closes: #123
2023-03-27 15:38:49 +02:00
Henrik Böving 628ef2878e fix: properly comment out for the workaround 2023-03-16 20:39:30 +01:00
F. G. Dorais 5ab7d0bdd8 fix: unicode dependency 2023-03-15 11:54:57 +01:00
Henrik Böving 0c415232cd feat: new CI setup 2023-03-12 13:19:02 +01:00
F. G. Dorais 755f06fb0d fix: correct character category testing 2023-03-11 21:14:36 +01:00
Henrik Böving 5f59fbaac4 refactor: switch to maintained unicode lib 2023-03-11 18:06:32 +01:00
Henrik Böving 720e1acf81 feat: show versions in index HTML 2023-03-09 21:46:38 +01:00
Max Taldykin c3faad1730 help break_within to split names at `.` 2023-03-04 12:47:30 +01:00
Henrik Böving 5ab6766eb1 fix: #113 2023-02-16 19:51:35 +01:00
Jeremy Salwen 1cb84f6d74 Add filters for search results based on kind.
This allows you to search defs, theorems, etc independently.
2023-02-01 15:15:45 +01:00
Henrik Böving 1c44e861be fix: search.html for relative roots 2023-01-29 14:07:21 +01:00
Jeremy Salwen 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
Jeremy Salwen 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
Henrik Böving a18b27f4c1 feat: attempt to improve usability of the file tree 2023-01-01 20:21:10 +01:00
Henrik Böving f74443a673 style: Lean 4 compiler style in output 2023-01-01 19:51:01 +01:00
Henrik Böving a5caefc03f fix: regression in import names 2023-01-01 18:59:19 +01:00
Seppel3210 03e6572584 fix: mention (a : α) → β a notation in foundational types section 2022-12-23 13:28:57 +01:00
Henrik Böving f221bbdcff fix: save the expansion state of the tree again 2022-12-13 20:01:11 +01:00
Henrik Böving 327fdf0ddd feat: short names in side bar 2022-12-13 19:37:28 +01:00
Henrik Böving 7009910876 chore: update toolchain 2022-12-03 17:43:12 +01:00
Henrik Böving 5e96952a58 chore: update toolchain 2022-12-02 17:55:27 +01:00
Henrik Böving 72034b0831 feat: linkify builtin types 2022-11-22 21:07:59 +01:00
Henrik Böving b22818b971 feat: render foundational types info 2022-11-22 21:07:59 +01:00
Alex J. Best 6137c9b300 Merge branch 'main' of github.com:leanprover/doc-gen4 into only-linkify-lean 2022-11-06 21:27:31 +01:00
Alex J. Best fc00a41ecb bool 2022-11-06 21:27:26 +01:00
Parth Shastri 664a86e08b fix: minor style improvements 2022-11-06 13:53:23 +01:00
Alex J. Best d62268b013 better 2022-11-05 18:46:20 +01:00
Alex J. Best 07cb0ed1cc fix 2022-11-05 18:28:27 +01:00
Alex J. Best 58fcc5d468 only linkify lean code 2022-11-05 18:18:16 +01:00