1.3 KiB
IDE protocol, version 2
The IDE protocol is (or rather, will be) compatible with the IDE protocol for Idris 1, as described here: https://idris.readthedocs.io/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.