@@ -46,13 +46,13 @@ This is achieved by the already seen ``:load-file`` command.
46The available commands include:
46The available commands include:
48 ``(:load-file FILENAME)``
48 ``(:load-file FILENAME)``
49− Load the named file
49+ Load the named file.
51 ``(:interpret STRING)``
51 ``(:interpret STRING)``
52− Interpret ``STRING`` at the Idris REPL, returning a highlighted result
52+ Interpret ``STRING`` at the Idris REPL, returning a highlighted result.
54 ``(:repl-completions STRING)``
54 ``(:repl-completions STRING)``
55− Return the result of tab-completing ``STRING`` as a REPL command
55+ Return the result of tab-completing ``STRING`` as a REPL command.
57 ``(:type-of STRING)``
57 ``(:type-of STRING)``
58 Return the type of the name, written with Idris syntax in the ``STRING``.
58 Return the type of the name, written with Idris syntax in the ``STRING``.
@@ -88,16 +88,16 @@ The available commands include:
88 List the currently-active holes, with their types pretty-printed with ``WIDTH`` columns.
88 List the currently-active holes, with their types pretty-printed with ``WIDTH`` columns.
90 ``(:who-calls NAME)``
90 ``(:who-calls NAME)``
91− Get a list of callers of ``NAME``
91+ Get a list of callers of ``NAME``.
93 ``(:calls-who NAME)``
93 ``(:calls-who NAME)``
94− Get a list of callees of ``NAME``
94+ Get a list of callees of ``NAME``.
96 ``(:browse-namespace NAMESPACE)``
96 ``(:browse-namespace NAMESPACE)``
97− Return the contents of ``NAMESPACE``, like ``:browse`` at the command-line REPL
97+ Return the contents of ``NAMESPACE``, like ``:browse`` at the command-line REPL.
99 ``(:normalise-term TM)``
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)
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)``
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.
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.
@@ -109,7 +109,10 @@ The available commands include:
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).
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)``
111 ``(:print-definition NAME)``
112− Return the definition of ``NAME`` as a highlighted string
112+ Return the definition of ``NAME`` as a highlighted string.
115+ Return the version information of the Idris compiler.