Commit Graph

265 Commits (a0779fa7dea952c8c77c1f71cdff9951fbf29c5d)

Author SHA1 Message Date
Henrik a090875215 refactor: Remove unnecessary cases in type analysis 2023-09-10 11:07:22 +02:00
Henrik 7dc8018130 refactor: Less manual manipulation of expressions 2023-09-10 10:13:30 +02:00
Henrik 6abc8bb769 feat: print location of errors during documentation 2023-09-10 01:02:52 +02:00
Henrik 8ea6a55a82 chore: print named instance arguments 2023-09-10 00:18:52 +02:00
Henrik 36e1b863a7 chore: remove pointless prints 2023-09-09 23:59:25 +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
Henrik 13fb60f8a3 feat: deprecated attr 2023-09-08 23:06:56 +02:00
tydeu 0b52010291 fix: source links for Lake 2023-08-30 19:01:03 +02:00
Henrik dc9549e2e6 feat: cleanup def rendering and add reducible attribute 2023-08-28 20:38:19 +02:00
tydeu 34165f36e6 feat: include Lake as part of the core docs 2023-08-24 10:10:16 +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 9b028566ec fix: get rid off deleted attribute 2023-04-16 09:54:48 +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 d5ef8006b7 style: Lean 4 compiler style in LeanInk 2023-01-01 19:53:21 +01:00
Henrik Böving f74443a673 style: Lean 4 compiler style in output 2023-01-01 19:51:01 +01:00
Henrik Böving 3a5c0db46b style: refactor process to Lean 4 compiler style 2023-01-01 19:30:28 +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 345036e800 chore: update toolchain 2022-12-22 16:19:23 +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
Henrik Böving e402ee94b1 feat: look for builtin type instances 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