@@ -46,13 +46,13 @@ This is achieved by the already seen ``:load-file`` command.
4646The available commands include:
4747
4848 ``(:load-file FILENAME)``
49− Load the named file
49+ Load the named file.
5050
5151 ``(:interpret STRING)``
52− Interpret ``STRING`` at the Idris REPL, returning a highlighted result
52+ Interpret ``STRING`` at the Idris REPL, returning a highlighted result.
5353
5454 ``(: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.
5656
5757 ``(:type-of STRING)``
5858 Return the type of the name, written with Idris syntax in the ``STRING``.
@@ -88,16 +88,16 @@ The available commands include:
8888 List the currently-active holes, with their types pretty-printed with ``WIDTH`` columns.
8989
9090 ``(:who-calls NAME)``
91− Get a list of callers of ``NAME``
91+ Get a list of callers of ``NAME``.
9292
9393 ``(:calls-who NAME)``
94− Get a list of callees of ``NAME``
94+ Get a list of callees of ``NAME``.
9595
9696 ``(: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.
9898
9999 ``(: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).
101101
102102 ``(:show-term-implicits TM)``
103103 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:
109109 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).
110110
111111 ``(:print-definition NAME)``
112− Return the definition of ``NAME`` as a highlighted string
112+ Return the definition of ``NAME`` as a highlighted string.
113+
114+ ``(:version UID)``
115+ Return the version information of the Idris compiler.
113116
114117
115118