Add bash completion file for Idris
This is far from perfect, but seems to work reasonbly well.
Also, the targets/libraries should probably not be hardcoded, but at this point
it's not clear how to dynamically generate this.
To use this add a `source $PATH_TO/idris.bash` to your `.bashrc`.
You need to have the bash-completion[1] package installed for this to work.
[1]: http://bash-completion.alioth.debian.org/
commit31f4e9f626f7ddfea7b2f7355460cb20f53dd872
authorIgnas Vyšniauskas <baliulia@gmail.com>
dateWed 26 Jun 2013, 00:24 (13 years ago)
parent1b589f8
contribs/tool-support/completion/idris.bashnew file+31
@@ -0,0 +1,31 @@
1+_idris() {
2+ local cur prev words opts LIBRARIES TARGETS
3+ _init_completion || return
4+
5+ opts=$(_parse_help "$1")
6+ LIBRARIES="effects"
7+ TARGETS="C Java bytecode javascript node"
8+
9+ case "${prev}" in
10+ -o)
11+ _filedir
12+ ;;
13+ -i|--ibcsubdir)
14+ _filedir -d
15+ ;;
16+ -p)
17+ COMPREPLY=( $(compgen -W "${LIBRARIES}" -- ${cur}))
18+ ;;
19+ --target)
20+ COMPREPLY=( $(compgen -W "${TARGETS}" -- ${cur}))
21+ ;;
22+ esac
23+
24+ if [[ $cur == -* ]]; then
25+ COMPREPLY=($(compgen -W "${opts}" -- ${cur}))
26+ return
27+ fi
28+
29+ _filedir '@(idr)'
30+} &&
31+complete -o default -F _idris idris