5The Idris REPL has two modes of interaction: a human-readable syntax designed for direct use in a terminal, and a machine-readable syntax designed for using Idris as a backend for external tools.
10The communication protocol is of asynchronous request-reply style: a single request from the client is handled by Idris at a time.
11Idris waits for a request on its standard input stream, and outputs the answer or answers to standard output.
12The result of a request can be either success, failure, or intermediate output; and furthermore, before the result is delivered, there might be additional meta-messages.
15A reply can consist of multiple messages: any number of messages to inform the user about the progress of the request or other informational output, and finally a result, either ``ok`` or ``error``.
17The wire format is the length of the message in characters, encoded in 6 characters hexadecimal, followed by the message encoded as S-expression (sexp).
18Additionally, each request includes a unique integer (counting upwards), which is repeated in all messages corresponding to that request.
20An example interaction from loading the file ``/home/hannes/empty.idr`` looks as follows on the wire:::
22 00002a((:load-file "/home/hannes/empty.idr") 1)
23 000039(:write-string "Type checking /home/hannes/empty.idr" 1)
24 000025(:set-prompt "/home/hannes/empty" 1)
25 000032(:return (:ok "Loaded /home/hannes/empty.idr") 1)
28The first message is the request from idris-mode to load the specific file, which length is hex 2a, decimal 42 (including the newline at the end).
29The request identifier is set to 1.
30The first message from Idris is to write the string ``Type checking /home/hannes/empty.idr``, another is to set the prompt to ``*/home/hannes/empty``.
31The answer, starting with ``:return`` is ``ok``, and additional information is that the file was loaded.
33There are three atoms in the wire language: numbers, strings, and symbols.
34The only compound object is a list, which is surrounded by parenthesis.
37 A ::= NUM | '"' STR '"' | ':' ALPHA+
38 S ::= A | '(' S* ')' | nil
40where ``NUM`` is either 0 or a positive integer, ``ALPHA`` is an alphabetical character, and ``STR`` is the contents of a string, with ``"`` escaped by a backslash.
41The atom ``nil`` is accepted instead of ``()`` for compatibility with some regexp pretty-printing routines.
43The state of the Idris process is mainly the active file, which needs to be kept synchronised between the editor and Idris.
44This is achieved by the already seen ``:load-file`` command.
46The available commands include:
48 ``(:load-file FILENAME)``
51 ``(:interpret STRING)``
52 Interpret ``STRING`` at the Idris REPL, returning a highlighted result
54 ``(:repl-completions STRING)``
55 Return the result of tab-completing ``STRING`` as a REPL command
58 Return the type of the name, written with Idris syntax in the ``STRING``.
59 The reply may contain highlighting information.
61 ``(:case-split LINE NAME)``
62 Generate a case-split for the pattern variable ``NAME`` on program line ``LINE``.
63 The pattern-match cases to be substituted are returned as a string with no highlighting.
65 ``(:add-clause LINE NAME)``
66 Generate an initial pattern-match clause for the function declared as ``NAME`` on program line ``LINE``.
67 The initial clause is returned as a string with no highlighting.
69 ``(:add-proof-clause LINE NAME)``
70 Add a clause driven by the ``<==`` syntax.
72 ``(:add-missing LINE NAME)``
73 Add the missing cases discovered by totality checking the function declared as ``NAME`` on program line ``LINE``.
74 The missing clauses are returned as a string with no highlighting.
76 ``(:make-with LINE NAME)``
77 Create a with-rule pattern match template for the clause of function ``NAME`` on line ``LINE``.
78 The new code is returned with no highlighting.
80 ``(:proof-search LINE NAME HINTS)``
81 Attempt to fill out the holes on ``LINE```named ``NAME`` by proof search.
82 ``HINTS`` is a possibly-empty list of additional things to try while searching.
85 Look up the documentation for ``NAME``, and return it as a highlighted string.
87 ``(:metavariables WIDTH)``
88 List the currently-active holes, with their types pretty-printed with ``WIDTH`` columns.
91 Get a list of callers of ``NAME``
94 Get a list of callees of ``NAME``
96 ``(:browse-namespace NAMESPACE)``
97 Return the contents of ``NAMESPACE``, like ``:browse`` at the command-line REPL
99 ``(:normalise-term TM)``
100 Return a highlighted string consisting of the results of normalising the serialised term ``TM`` (which would previously have been sent as the ``tt-term`` property of a string)
102 ``(:show-term-implicits TM)``
103 Return a highlighted string consisting of the results of making all arguments in serialised term ``TM`` (which would previously have been sent as the ``tt-term`` property of a string) explicit.
105 ``(:hide-term-implicits TM)``
106 Return a highlighted string consisting of the results of making all arguments in serialised term ``TM`` (which would previously have been sent as the ``tt-term`` property of a string) follow their usual implicitness setting.
108 ``(:elaborate-term TM)``
109 Return a highlighted string consisting of the the core language term corresponding to serialised term ``TM`` (which would previously have been sent as the ``tt-term`` property of a string).
111 ``(:print-definition NAME)``
112 Return the definition of ``NAME`` as a highlighted string
116Possible replies include a normal final reply:::
118 (:return (:ok SEXP [HIGHLIGHTING]))
119 (:return (:error String [HIGHLIGHTING]))
121A normal intermediate reply:::
123 (:output (:ok SEXP [HIGHLIGHTING]))
124 (:output (:error String [HIGHLIGHTING]))
126Informational and/or abnormal replies:::
128 (:write-string String)
130 (:warning (FilePath (LINE COL) (LINE COL) String [HIGHLIGHTING]))
135 (:write-proof-state [String] [HIGHLIGHTING])
142Idris mode supports highlighting the output from Idris.
143In reality, this highlighting is controlled by the Idris compiler.
144Some of the return forms from Idris support an optional extra parameter: a list mapping spans of text to metadata about that text.
145Clients can then use this list both to highlight the displayed output and to enable richer interaction by having more metadata present.
146For example, the Emacs mode allows right-clicking identifiers to get a menu with access to documentation and type signatures.
149A particular semantic span is a three element list.
150The first element of the list is the index at which the span begins, the second element is the number of characters included in the span, and the third is the semantic data itself.
151The semantic data is a list of lists.
152The head of each list is a key that denotes what kind of metadata is in the list, and the tail is the metadata itself.
154The following keys are available:
156 gives a reference to the fully-qualified Idris name
158 provides a Boolean value that is True if the region is the name of an implicit argument
160 describes the category of a token, which can be ``type``, ``function``, ``data``, ``keyword``, or ``bound``.
163 states that the region refers to a source code location. Its body is a collection of key-value pairs, with the following possibilities:
166 provides the filename
169 provides the line and column that the source location starts at as a two-element tail
172 provides the line and column that the source location ends at as a two-element tail
175 provides an attribute of formatted text. This is for use with natural-language text, not code, and is presently emitted only from inline documentation. The potential values are ``bold``, ``italic``, and ``underline``.
178 provides a URL that the corresponding text is a link to.
181 states that the region is quasiquoted.
184 states that the region is antiquoted.
187 A serialised representation of the Idris core term corresponding to the region of text.
189Source Code Highlighting
190------------------------
192Idris supports instructing editors how to colour their code.
193When elaborating source code or REPL input, Idris will locate regions of the source code corresponding to names, and emit information about these names using the same metadata as output highlighting.
195These messages will arrive as replies to the command that caused elaboration to occur, such as ``:load-file`` or ``:interpret``.
196They have the format:::
198 (:output (:ok (:highlight-source POSNS)))
200where ``POSNS`` is a list of positions to highlight. Each of these is a two-element list whose first element is a position (encoded as for the ``source-loc`` property above) and whose second element is highlighting metadata in the same format used for output.
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list