|
|
1ccccb370b
|
Don't select the current node in select_nodes
|
2023-11-13 18:46:34 +01:00 |
|
|
|
32a77b3a31
|
Change behaviour of next and previous node
|
2023-11-12 23:08:35 +01:00 |
|
|
|
6e6ad7a82b
|
Default config
|
2023-11-12 22:54:56 +01:00 |
|
|
|
374910704d
|
Change select-children to not use nodes_in_range
|
2023-11-12 22:17:04 +01:00 |
|
|
|
326cb00da5
|
Change selection to have anchor at the start
|
2023-11-12 20:06:26 +01:00 |
|
|
|
1314dce07d
|
Ignore unnamed nodes
|
2023-11-12 17:26:53 +01:00 |
|
|
|
fc7288a27f
|
tree-select-node to select current node
|
2023-11-12 17:26:44 +01:00 |
|
|
|
a78febec6c
|
Highlight current node
|
2023-11-12 17:26:31 +01:00 |
|
|
|
0acc4dbba4
|
Add agda, nix
|
2023-11-12 14:36:27 +01:00 |
|
|
|
d62b1657c3
|
Try to load language for --do-you-understand
|
2023-11-12 11:42:22 +01:00 |
|
|
|
f193be1731
|
First commit
|
2023-11-12 00:21:50 +01:00 |
|
