|
|
9c35464b69
|
also print input expression with \e
|
2023-05-28 14:44:12 +02:00 |
|
|
|
2c89714506
|
remove commands that don't exist in idris2
|
2023-05-28 14:43:45 +02:00 |
|
|
|
518e5f0c41
|
fix refine command
|
2023-05-27 16:22:20 +02:00 |
|
|
|
ad08ee24f5
|
stop wobbling the window around on reload
|
2023-05-27 16:22:13 +02:00 |
|
|
|
f89aa275a1
|
abstract isn't reserved
|
2023-02-25 16:45:17 +01:00 |
|
|
|
2b35029bde
|
raw strings
|
2022-04-11 14:10:49 +02:00 |
|
|
|
f248ccb909
|
add 'proof' keyword
|
2022-01-04 16:34:40 +01:00 |
|
|
|
5a42b26e80
|
add %search
|
2022-01-03 22:46:04 +01:00 |
|
|
|
6b8e2c8d3e
|
else if → elseif
|
2022-01-03 15:09:55 +01:00 |
|
|
|
1e64a7bd2c
|
set more scratch props for idris-response
|
2022-01-03 15:09:43 +01:00 |
|
|
|
9725d2273e
|
add \> after %keywords
|
2021-12-30 13:51:17 +01:00 |
|
|
|
01ae8cf8e4
|
remove duplicate %defaulthint
|
2021-12-29 10:24:09 +01:00 |
|
|
|
99bba8a3fd
|
fix typo in %ambiguity_depth
|
2021-12-29 10:23:45 +01:00 |
|
|
|
b6f26d5e7e
|
add %builtin
|
2021-12-29 10:23:25 +01:00 |
|
|
|
71d9ecb0c5
|
add \T to readme
|
2021-12-28 09:58:08 +01:00 |
|
|
|
555d6bf79a
|
don't highlight the insides of braces
|
2021-12-28 09:56:16 +01:00 |
|
|
|
be255abde7
|
don't clobber registers with old idris-response
|
2021-12-28 09:56:16 +01:00 |
|
|
|
3ffa41df09
|
remove } from indk
|
2021-12-28 09:56:16 +01:00 |
|
|
|
58d3843ef1
|
add idiom brackets
|
2021-12-28 09:56:16 +01:00 |
|
|
|
f088d05a14
|
add \T to show type with implicits
|
2021-12-28 09:56:16 +01:00 |
|
Edwin Brady
|
964cebee49
|
Merge pull request #16 from ShinKage/disable-color
Disable color and minor syntax additions
|
2020-11-26 15:50:07 +00:00 |
|
Giuseppe Lomurno
|
20f025a225
|
Disable color and minor syntax additions
|
2020-08-20 10:52:07 +02:00 |
|
Edwin Brady
|
099129e08c
|
Merge pull request #8 from ShinKage/idris2-syntax
Updated idris2 syntax highlighting
|
2020-05-25 11:53:38 +01:00 |
|
Edwin Brady
|
2f1a013414
|
Merge pull request #7 from buzden/further-secondification
Further "Idris" -> "Idris 2" renamings were done
|
2020-05-25 11:53:08 +01:00 |
|
Edwin Brady
|
7254ad0cde
|
Merge pull request #5 from neriglissar/neriglissar/fix-IdrisReload
[Fix] E121: Undefined variable: file in IdrisReload
|
2020-05-25 11:52:26 +01:00 |
|
Giuseppe Lomurno
|
05cdd9ff47
|
Added %tcinline pragma
|
2020-05-22 18:18:37 +02:00 |
|
Giuseppe Lomurno
|
2013a7129c
|
Updated idris2 syntax highlighting
|
2020-05-19 20:40:40 +02:00 |
|
Denis Buzdalov
|
874495a339
|
Further "Idris" -> "Idris 2" renamings were done
|
2020-05-19 18:32:37 +03:00 |
|
neriglissar
|
5f31ebb697
|
[Fix] E121: Undefined variable: file in IdrisReload
|
2020-05-17 14:15:08 +02:00 |
|
Edwin Brady
|
b057b734aa
|
Merge pull request #4 from ShinKage/path-escape
Escape the paths passed to idris2
|
2020-05-15 15:16:26 +01:00 |
|
Giuseppe Lomurno
|
bd97999479
|
Escape the paths passed to idris2
|
2020-05-15 15:33:33 +02:00 |
|
Edwin Brady
|
0fd4094cc3
|
Merge pull request #2 from ziman/absolute-paths
Use absolute paths to invoke Idris2
|
2020-04-01 00:53:30 +01:00 |
|
Matus Tejiscak
|
8a8c94d328
|
Use absolute paths to invoke Idris2.
|
2020-03-29 18:30:25 +02:00 |
|
Edwin Brady
|
9333d92ffa
|
Merge pull request #1 from mrkgnao/patch-1
fix references to idris1(-mode) in README.md
|
2020-03-10 11:43:45 +00:00 |
|
Soham Chowdhury
|
a1ea598326
|
fix references to idris1(-mode)
|
2020-03-10 08:13:16 +05:30 |
|
Edwin Brady
|
7a0b10df22
|
Add --find-ipkg flag
This means the Idris instance will look for an ipkg file in parent
directories and use that as the root, processing any options.
|
2020-02-23 12:56:29 +00:00 |
|
Edwin Brady
|
0db674ff18
|
More README fixes
|
2020-02-22 20:46:22 +00:00 |
|
Edwin Brady
|
16eaa95de4
|
Update README slightly
|
2020-02-22 20:45:05 +00:00 |
|
Edwin Brady
|
2d3f31df29
|
Rename to idris2
|
2020-02-22 20:34:56 +00:00 |
|
Edwin Brady
|
e3816a7be5
|
Initial version
Mostly copied from idris-vim
|
2020-02-22 20:32:56 +00:00 |
|
