@@ -45,8 +45,8 @@ This is achieved by the already seen ``:load-file`` command.
4545
4646The available commands include:
4747
48− ``(:load-file FILENAME)``
49− Load the named file.
48+ ``(:load-file FILENAME [LINE])``
49+ Load the named file. If a ``LINE`` number is provided, the file is only loaded up to that line. Otherwise, the entire file is loaded.
5050
5151 ``(:interpret STRING)``
5252 Interpret ``STRING`` at the Idris REPL, returning a highlighted result.
@@ -88,9 +88,12 @@ The available commands include:
8888 Attempt to fill out the holes on ``LINE`` named ``NAME`` by proof search.
8989 ``HINTS`` is a possibly-empty list of additional things to try while searching.
9090
91− ``(:docs-for NAME)``
92− Look up the documentation for ``NAME``, and return it as a highlighted string.
93−
91+ ``(:docs-for NAME [MODE])``
92+ Look up the documentation for ``NAME``, and return it as a highlighted string. If ``MODE`` is ``:overview``, only the first paragraph of documentation is provided for ``NAME``. If ``MODE`` is ``:full``, or omitted, the full documentation is returned for ``NAME``.
93+
94+ ``(:apropos STRING)``
95+ Search the documentation for mentions of ``STRING``, and return any found as a list of highlighted strings.
96+
9497 ``(:metavariables WIDTH)``
9598 List the currently-active holes, with their types pretty-printed with ``WIDTH`` columns.
9699
@@ -121,7 +124,7 @@ The available commands include:
121124 ``(:repl-completions NAME)``
122125 Search names, types and documentations which contain ``NAME``.
123126
124− ``(:version UID)``
127+ ``:version``
125128 Return the version information of the Idris compiler.
126129
127130