f9d9875671
perf: Don't call Lake from within doc-gen anymore
2023-10-09 09:30:16 +02:00
96870507c5
feat: add jump-src.js for #src links
2023-09-21 11:38:22 +02:00
924be4c7d8
feat: expand the current file in the navbar
2023-09-18 23:55:19 +02:00
36e1b863a7
chore: remove pointless prints
2023-09-09 23:59:25 +02:00
718b182a31
feat: more declaration data as JSON
2023-08-06 15:36:43 +02:00
cc552ed570
add colorscheme toggle
2023-06-09 23:39:59 +02:00
720e1acf81
feat: show versions in index HTML
2023-03-09 21:46:38 +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
b22818b971
feat: render foundational types info
2022-11-22 21:07:59 +01:00
64f627a295
chore: toolchain upgrade ( #82 )
...
Halleluja!
2022-10-05 12:05:58 +02:00
14afcdbeaf
feat: Degrade --ink to flag
2022-07-26 13:56:22 +02:00
5a893f4b76
feat: LeanInk backlink step 1
2022-07-26 12:52:41 +02:00
5e634cf96a
feat: typify the index API
2022-07-25 09:47:59 +02:00
247b930364
feat: instances for
2022-07-23 15:40:08 +02:00
ed4cee2eae
chore: style, change $ to <|
2022-07-23 13:01:25 +02:00
95b79c1744
fix: Fix linking of importedBy modules
2022-07-22 17:03:24 +02: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
bb9b55ef2c
feat: Step 1 for full separate builds with global info
2022-07-22 14:48:36 +02:00
eea23d332a
feat: Fully separated builds
2022-07-21 22:43:33 +02:00
80cb92eb94
feat: Use iframe for navbar to move it into the finalize stage
2022-07-21 22:06:26 +02:00
80cf5bc96f
feat: Renamed finalize to index
2022-07-21 21:19:37 +02:00
71af8db54b
feat: Declaration data into separate directory
2022-07-21 21:05:19 +02:00
9b2326dec3
feat: merge init and finalize
2022-07-21 19:07:35 +02:00
4bc7a682ec
feat: implementation of separate staged builds
2022-07-21 18:26:01 +02:00
fbbdb21795
fix: remove redundant argument
2022-07-21 02:25:26 +02:00
9962e5037a
prettify: Make the Output.lean refactor prettier
2022-07-21 02:21:07 +02:00
25b1ddb66b
feat: Preparations to split doc-gen build process
2022-07-21 01:40:04 +02:00
be3caa9e1a
feat: Basic semantic highlighting support
2022-06-20 22:21:48 +02:00
9f50966339
feat: initial LeanInk HTML generation
2022-06-20 18:39:55 +02:00
199c7af17a
feat: LeanInk all the files, HTML generation missing
2022-06-20 00:31:09 +02:00
d519ef6b58
fix: adapt the rest of the program to the process refactor
2022-05-20 00:36:43 +02:00
0b8f7a1397
doc: Output top level module
2022-05-19 20:54:42 +02:00
43f7786523
refactor: pull source linker into submodule
2022-05-19 20:48:26 +02:00
3ac6ddd1ab
fix: port the SITE_ROOT fix to find.js
2022-04-07 13:14:01 +02:00
67402506c7
fix: links in search
2022-04-07 12:44:33 +02:00
06c20ee46f
dynamically change SITE_ROOT since we are relative now
2022-04-07 12:39:32 +02:00
4bc149a1fb
Fix diff nits
2022-04-07 00:53:06 +01:00
9570f25312
cleanup code
2022-04-07 00:48:12 +01:00
9eec1cf1ad
URLs now work; Data fetching does not?
2022-04-07 00:31:27 +01:00
9cc4c787e6
feat: lake integration
2022-03-06 18:51:06 +01:00
2b217ecda0
fix: fix find search
2022-02-23 05:32:37 +08:00
a18e343829
refactor: change find syntax
2022-02-23 04:26:20 +08:00
004977e6e4
refactor: use strict match for find
2022-02-22 15:01:14 +08:00
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
Henrik Böving
Mario Carneiro
Alex J. Best
Calvin Lee
Jeremy Salwen
Siddharth Bhat
Xubai Wang