Commit Graph

32 Commits (main)

Author SHA1 Message Date
Alex J Best 5b4d779b31 Update DocGen4/Output/DocString.lean 2023-10-16 20:42:29 +02:00
Alex J. Best 074c783259 feat: html escape docstrings 2023-10-16 20:42:29 +02:00
Ruben Van de Velde 19568c0659 feat: autolink references to files 2023-09-16 14:37:22 +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 Böving b9421b9a12 fix: Use Z(separator) instead of S(ymbol) category
closes: #123
2023-03-27 15:38:49 +02:00
F. G. Dorais 5ab7d0bdd8 fix: unicode dependency 2023-03-15 11:54:57 +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 5ab6766eb1 fix: #113 2023-02-16 19:51:35 +01:00
Henrik Böving f74443a673 style: Lean 4 compiler style in output 2023-01-01 19:51:01 +01:00
Alex J. Best fc00a41ecb bool 2022-11-06 21:27:26 +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
Mario Carneiro 9aef28b16e
chore: update toolchain 10-20 (#86) 2022-10-20 19:51:26 +02:00
Henrik Böving 64f627a295
chore: toolchain upgrade (#82)
Halleluja!
2022-10-05 12:05:58 +02:00
Gabriel Ebner 9dc1889de6 chore: update toolchain 2022-08-18 11:33:49 +02:00
Henrik Böving 04387711de chore: remove unused variables 2022-07-23 13:04:36 +02:00
Henrik Böving ed4cee2eae chore: style, change $ to <| 2022-07-23 13:01:25 +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 89dd2fa46e chore: upgrade compiler version 2022-04-09 19:30:33 +02:00
Xubai Wang 2151813fe5 feat: allow intra link in code block 2022-02-20 13:28:48 +08:00
Xubai Wang ad4d77a9c9 fix: change same end maching 2022-02-20 11:43:27 +08:00
Xubai Wang 3acfc510b4 fix: no overmatch for intra link 2022-02-20 03:28:03 +08:00
Xubai Wang 5e550c7833 refactor: docstring between basic and extra info
clean up code
2022-02-20 03:14:58 +08:00
Xubai Wang cce4285c96 fix: intersperse code contents 2022-02-18 04:01:31 +08:00
Xubai Wang 9550d1c92e refactor: use ## for intra doc 2022-02-18 03:26:38 +08:00
Xubai Wang 0b9a9f0bdc fix: remove intra link in code block 2022-02-18 01:39:02 +08:00
Xubai Wang 11bb2af57a feat: add auto link 2022-02-18 00:46:02 +08:00
Xubai Wang 97ddf05ab6 fix: add root to relative href 2022-02-17 21:26:02 +08:00
Xubai Wang 1729f4aa71 fix: fix docstring heading id 2022-02-17 15:26:17 +08:00
Xubai Wang b7c6a98969 refactor: separate docstring code 2022-02-17 13:47:38 +08:00