@@ -27,7 +27,7 @@ An example interaction from loading the file ``/home/hannes/empty.idr`` looks as
2727
2828The 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).
2929The request identifier is set to 1.
30−The 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''.
30+The 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``.
3131The answer, starting with ``:return`` is ``ok``, and additional information is that the file was loaded.
3232
3333There are three atoms in the wire language: numbers, strings, and symbols.
@@ -188,4 +188,4 @@ They have the format:::
188188
189189 (:output (:ok (:highlight-source POSNS)))
190190
191−where ``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.
191+where ``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.