@@ -27,7 +27,7 @@ An example interaction from loading the file ``/home/hannes/empty.idr`` looks as
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).
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.
29The 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``.
31The answer, starting with ``:return`` is ``ok``, and additional information is that the file was loaded.
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.
33There are three atoms in the wire language: numbers, strings, and symbols.
@@ -188,4 +188,4 @@ They have the format:::
189 (:output (:ok (:highlight-source POSNS)))
189 (:output (:ok (:highlight-source POSNS)))
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.