@@ -45,8 +45,8 @@ 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 [LINE])``
49− Load the named file.
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.
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.
@@ -88,9 +88,12 @@ The available commands include:
88 Attempt to fill out the holes on ``LINE`` named ``NAME`` by proof search.
88 Attempt to fill out the holes on ``LINE`` named ``NAME`` by proof search.
89 ``HINTS`` is a possibly-empty list of additional things to try while searching.
89 ``HINTS`` is a possibly-empty list of additional things to try while searching.
91− ``(:docs-for NAME)``
91+ ``(:docs-for NAME [MODE])``
92− Look up the documentation for ``NAME``, and return it as a highlighted string.
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``.
94+ ``(:apropos STRING)``
95+ Search the documentation for mentions of ``STRING``, and return any found as a list of highlighted strings.
94 ``(:metavariables WIDTH)``
97 ``(:metavariables WIDTH)``
95 List the currently-active holes, with their types pretty-printed with ``WIDTH`` columns.
98 List the currently-active holes, with their types pretty-printed with ``WIDTH`` columns.
@@ -121,7 +124,7 @@ The available commands include:
121 ``(:repl-completions NAME)``
124 ``(:repl-completions NAME)``
122 Search names, types and documentations which contain ``NAME``.
125 Search names, types and documentations which contain ``NAME``.
124− ``(:version UID)``
127+ ``:version``
125 Return the version information of the Idris compiler.
128 Return the version information of the Idris compiler.