git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3349 from jfdm/bash-completion-info
1aba372Jan de Muijnck-Hughes
docs/reference/misc.rst+25−2
compare with master
unifiedsplit
@@ -169,7 +169,7 @@ Usage from C code
169* Feel free to mutate both the pointer ``data`` (eg. after calling ``realloc``)
169* Feel free to mutate both the pointer ``data`` (eg. after calling ``realloc``)
170 and the memory it points to. However, keep in mind
170 and the memory it points to. However, keep in mind
171 that this must not break Idris's referential transparency.
171 that this must not break Idris's referential transparency.
172−
172+
173* **WARNING!** If you call ``cdata_allocate`` or ``cdata_manage``,
173* **WARNING!** If you call ``cdata_allocate`` or ``cdata_manage``,
174 the resulting ``CData`` object *must* be returned from your
174 the resulting ``CData`` object *must* be returned from your
175 FFI function so that it is inserted in the C heap by the RTS.
175 FFI function so that it is inserted in the C heap by the RTS.
@@ -184,7 +184,7 @@ Usage from C code
184 other_fun cd i = foreign FFI_C "other_fun" (CData -> Int -> IO Int) cd i
184 other_fun cd i = foreign FFI_C "other_fun" (CData -> Int -> IO Int) cd i
185
185
186.. code:: cpp
186.. code:: cpp
187−
187+
188 #include "idris_rts.h"
188 #include "idris_rts.h"
189
189
190 static void finalizer(void * data)
190 static void finalizer(void * data)
@@ -310,3 +310,26 @@ Reflection
310Including ``%reflection`` functions and ``quoteGoal x by fn in t``,
310Including ``%reflection`` functions and ``quoteGoal x by fn in t``,
311which applies ``fn`` to the expected type of the current expression, and
311which applies ``fn`` to the expected type of the current expression, and
312puts the result in ``x`` which is in scope when elaborating ``t``.
312puts the result in ``x`` which is in scope when elaborating ``t``.
313+
314+Bash Completion
315+================
316+
317+Use of ``optparse-applicative`` allows Idris to support Bash
318+completion. You can obtain the completion script for Idris using the
319+following command::
320+
321+ idris --bash-completion-script `which idris`
322+
323+
324+To enable completion for the lifetime of your current session, run the
325+following command::
326+
327+ source <(idris --bash-completion-script `which idris`)
328+
329+
330+To enable completion permenatly you must either:
331+
332+* Modify your bash init script with the above command.
333+
334+* Add the completion script to the appropriate ``bash_completion.d/``
335+ folder on your machine.