mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-30 22:05:32 +03:00
44 lines
1.3 KiB
Markdown
44 lines
1.3 KiB
Markdown
IDE protocol, version 2
|
|
=======================
|
|
|
|
The IDE protocol is (or rather, will be) compatible with the IDE protocol for
|
|
Idris 1, as described here:
|
|
http://docs.idris-lang.org/en/latest/reference/ide-protocol.html
|
|
|
|
On start up, it reports:
|
|
|
|
`000018(:protocol-version 2 0)`
|
|
|
|
So far, there are two extended commands and one new command.
|
|
|
|
Extended commands
|
|
-----------------
|
|
|
|
`(:type-of STRING LINE COLUMN)`
|
|
|
|
If `type-of` is given a line and a column, this looks up the type of the name
|
|
at that location, which may be a local variable or a specialisation of a
|
|
global definition.
|
|
|
|
`(:proof-search LINE NAME HINTS :all)`
|
|
|
|
The optional additional argument `:all` means that the expression search will
|
|
return all of the results it finds, one per line (up to a currently hard coded
|
|
search depth limit, which will probably be settable as an option in the
|
|
future).
|
|
|
|
`(:case-split LINE COLUMN NAME)`
|
|
|
|
Case splitting can take an optional additional `COLUMN` argument.
|
|
|
|
New commands
|
|
------------
|
|
|
|
`(:generate-def LINE NAME)`
|
|
|
|
Generates a pattern matching definition, if it can find one, for the function
|
|
declared with the given name, on the given line. It will only return the
|
|
first definition it finds, as a list of pattern clauses. This works via a
|
|
combination of case splitting and expression search.
|
|
|