@@ -77,8 +77,15 @@ The available commands include:
7777 Create a with-rule pattern match template for the clause of function ``NAME`` on line ``LINE``.
7878 The new code is returned with no highlighting.
7979
80+ ``(:make-case LINE NAME)``
81+ Create a case pattern match template for the clause of function ``NAME`` on line ``LINE``.
82+ The new code is returned with no highlighting.
83+
84+ ``(:make-lemma LINE NAME)``
85+ Create a top level function with a type which solves the hole named ``NAME`` on line ``LINE``.
86+
8087 ``(:proof-search LINE NAME HINTS)``
81− 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.
8289 ``HINTS`` is a possibly-empty list of additional things to try while searching.
8390
8491 ``(:docs-for NAME)``
@@ -111,6 +118,9 @@ The available commands include:
111118 ``(:print-definition NAME)``
112119 Return the definition of ``NAME`` as a highlighted string.
113120
121+ ``(:repl-completions NAME)``
122+ Search names, types and documentations which contain ``NAME``.
123+
114124 ``(:version UID)``
115125 Return the version information of the Idris compiler.
116126