Commit Graph

56 Commits (main)

Author SHA1 Message Date
Joshua Potter cda229ac12 Add nameext to distinguish PDF and HTML files. 2023-12-14 17:09:10 -07:00
Henrik Böving b85fd6cbeb fix: lake changed the build directory 2023-11-18 23:11:44 +01:00
Henrik Böving f9d9875671 perf: Don't call Lake from within doc-gen anymore 2023-10-09 09:30:16 +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 f7307953d8 fix: sort expression printing 2023-09-10 14:44:14 +02:00
Calvin Lee cc552ed570 add colorscheme toggle 2023-06-09 23:39:59 +02: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 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
Henrik Böving 327fdf0ddd feat: short names in side bar 2022-12-13 19:37:28 +01:00
Henrik Böving 72034b0831 feat: linkify builtin types 2022-11-22 21:07:59 +01:00
Henrik Böving d43b23ec9f fix: Dont linkify unknown names 2022-08-11 23:35:43 +02:00
Henrik Böving 6534a71cca chore: update toolchain 2022-08-11 18:30:28 +02:00
Henrik Böving 5bae061b54 fix: mess of monad transformers in LeanInk adapter 2022-07-27 20:11:41 +02:00
Henrik Böving 0ac64f0873 types, types everywhere 2022-07-26 16:26:16 +02:00
Henrik Böving 5a893f4b76 feat: LeanInk backlink step 1 2022-07-26 12:52:41 +02:00
Henrik Böving ed4cee2eae chore: style, change $ to <| 2022-07-23 13:01:25 +02:00
Henrik Böving 19ee7dfd97 fix: Safari issues reported by Wojciech Nawrocki 2022-07-22 17:27:35 +02:00
Henrik Böving 2ffff99f90 feat: instances from JSON 2022-07-22 16:15:37 +02:00
Henrik Böving bb9b55ef2c feat: Step 1 for full separate builds with global info 2022-07-22 14:48:36 +02:00
Henrik Böving 0cff3d7cda fix: Javascript errors in the navbar 2022-07-21 23:01:15 +02:00
Henrik Böving 80cb92eb94 feat: Use iframe for navbar to move it into the finalize stage 2022-07-21 22:06:26 +02:00
Henrik Böving 25b1ddb66b feat: Preparations to split doc-gen build process 2022-07-21 01:40:04 +02:00
Henrik Böving 5f45c8dadc chore: update toolchain 2022-07-20 16:29:18 +02:00
Henrik Böving 5b56be76f2 chore: Cleanup HTML syntax and pretty printing 2022-06-21 20:54:29 +02:00
Henrik Böving be3caa9e1a feat: Basic semantic highlighting support 2022-06-20 22:21:48 +02:00
Henrik Böving 9f50966339 feat: initial LeanInk HTML generation 2022-06-20 18:39:55 +02:00
Henrik Böving 199c7af17a feat: LeanInk all the files, HTML generation missing 2022-06-20 00:31:09 +02:00
Henrik Böving d519ef6b58 fix: adapt the rest of the program to the process refactor 2022-05-20 00:36:43 +02:00
Henrik Böving 20e136bb27 refactor: centralized methods for internal linking infrastructure 2022-05-19 21:49:16 +02:00
Henrik Böving bdd4a5f612 doc: Output.Base 2022-05-19 21:05:17 +02:00
Henrik Böving 279df92555 refactor: restructure the modules 2022-05-19 20:41:07 +02:00
Henrik Böving 89dd2fa46e chore: upgrade compiler version 2022-04-09 19:30:33 +02:00
Henrik Böving 06c20ee46f dynamically change SITE_ROOT since we are relative now 2022-04-07 12:39:32 +02:00
Siddharth Bhat 4bc149a1fb Fix diff nits 2022-04-07 00:53:06 +01:00
Siddharth Bhat 9eec1cf1ad URLs now work; Data fetching does not? 2022-04-07 00:31:27 +01:00
Xubai Wang 5f7d380ab7 refactor: make include_str relative to file 2022-02-26 09:41:25 +08:00
Henrik Böving 9dd5e316c1
Merge pull request #38 from xubaiw/win-find
Windows find support among other things.
2022-02-23 19:44:47 +01:00
Xubai Wang f23556739f refactor: clean up javascript code 2022-02-22 12:40:14 +08:00
Xubai Wang 9e867f5151 refactor: make site-root an actual file 2022-02-21 23:29:23 +08:00
Siddharth Bhat 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
Xubai Wang 59707cda58 refactor: use js for find 2022-02-21 01:12:49 +08:00
Henrik Böving 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
Xubai Wang 5dc3ab855f feat: config mathjax like doc-gen 2022-02-18 03:27:00 +08:00
Henrik Böving 4b9b7d77d5 chore: Update doc-gen search js 2022-02-13 14:25:37 +01:00
Henrik Böving d39b14cf7a chore: bump toolchain, bye auto pure 2022-02-12 15:09:13 +01:00
Henrik Böving 735bfa35a7 chore: update compiler version 2022-01-15 15:35:52 +01:00
Henrik Böving f7f8138e09 feat: basic source links 2022-01-14 13:36:41 +01:00