Le Lundi 26 Septembre 2011 18:54:37 Gerwin Klein a écrit :
> On 26/09/2011, at 6:43 PM, Florian Haftmann wrote:
> > An aside: have there ever been thoughts about adding subcommand
> > completion for isabelle in bash? At first sight this looks as a nice
> > thing to have, but maybe there have been deeper consideration *not* to
> > attempt this.
>
> I've been using the attached for a few years. Just load as part of your
> ~/.bashrc or similar.
>
> It does 'isabelle make' target completion as well (code based on make
> completion from bash back then).
>
> It probably needs a thorough code review before it can be put anywhere
> official. I've mostly used it just for myself, even though I think I sent
> it to isabelle-users at some point.
I've also been using my attached configuration for some time. I did try to be
exhaustive on the subcommands and options, following the isabelle command
help. I don't know how it compares to yours, but they could possibly be
merged. I also think mine should be reviewed deeply, but it worked well for
me.
Regards,
Mathieu
# vim: set ft=sh ts=2 sw=2 et:
# file: /etc/bash_completion.d/isabelle
# Bash completion for isabelle
# Original: Mathieu Giorgino <[email protected]>
#
# Distributed under the terms of the GNU General Public License, v2 or later.
#
## isabelle completion
_isabelle_logic()
{
COMPREPLY=( $(compgen -W "$(isabelle findlogics)" -- $cur))
}
_isabelle()
{
local cur prev
COMPREPLY=()
cur=`_get_cword`
cur=${cur//\\\\/}
prev=${COMP_WORDS[COMP_CWORD-1]}
tool=${COMP_WORDS[1]}
# first parameter on line ?
if [ $COMP_CWORD -eq 1 ]; then
COMPREPLY=( $(compgen -W 'browser codegen dimacs2hol display
doc document emacs \
env findlogics getenv install java jedit keywords latex \
logo make makeall mkdir mkproject print mutabelle\
scala tty unsymbolize usedir version yxml mirabelle wwwfind'
-- $cur))
else
case $tool in
"browser")
if [[ "$cur" == -* ]]; then
COMPREPLY=( $(compgen -W '-c -o' --
$cur))
fi
_filedir
;;
"codegen")
if [ $COMP_CWORD -eq 2 ]; then
_isabelle_logic
elif [ $COMP_CWORD -eq 3 ]; then
_filedir thy
COMPREPLY=( ${COMPREPLY[@]%.thy} )
# elif [ $COMP_CWORD -eq 4 ]; then
#CMD in Isar command 'export_code CMD'
fi
;;
"dimacs2hol")
_filedir
;;
"display")
if [[ "$cur" == -* ]]; then
COMPREPLY=( $(compgen -W '-c' -- $cur))
else
_filedir
fi
;;
"doc")
if [ $COMP_CWORD -eq 2 ]; then
COMPREPLY=( $(compgen -W '$(isabelle
doc | grep -e "^ *" | sed "s/^ \(\S*\)\s\s*.*/\1/")' -- $cur))
fi
;;
"document")
opt_end="true"
if [[ "$prev" == -* ]]; then
opt_end="false"
case $prev in
-o)
COMPREPLY=( $(compgen
-W 'dvi dvi.gz ps ps.gz pdf' -- $cur))
;;
-c)
opt_end="true"
;;
# -n -t
esac
fi
if [ $opt_end == "true" ]; then
if [[ "$cur" == -* ]]; then
COMPREPLY=( $(compgen -W '-c -o
-n -t' -- $cur))
else
_filedir -d
fi
fi
;;
"emacs")
if [[ "$prev" == -* ]]; then
case $prev in
-I|-P|-U|-X|-u|-w|-x)
COMPREPLY=( $(compgen
-W 'true false' -- $cur))
;;
-L|-l|-k)
_isabelle_logic
;;
# -f -g -m -p
esac
elif [[ "$cur" == -* ]]; then
COMPREPLY=( $(compgen -W '-I -L -P -U
-X -f -g -k -l -m -p -u -w -x' -- $cur))
else
_filedir thy
fi
;;
"env")
COMPREPLY=( $(compgen -A command $cur))
;;
"findlogics")
;;
"logo")
if [[ "$cur" == -* ]]; then
COMPREPLY=( $(compgen -W '-o -q' --
$cur))
elif [[ "$cur" == "-o" ]]; then
_filedir
fi
;;
"make")
_make
COMPREPLY=( ${COMPREPLY[@]} $(compgen -W
'IsaMakefile' -- $cur ))
;;
"usedir")
if [[ "$prev" == -[^br] ]]; then
case $prev in
-C|-c|-Q|-g|-i|-v) #BOOL
COMPREPLY=( $(compgen
-W 'true false' -- $cur))
;;
-D|-P) #PATH
_filedir -d
;;
-f) #*..ML file
_filedir ML
;;
-s|-m) #NAME
;;
#-M -T -p -V -d
esac
elif [[ "$cur" == -* ]]; then
COMPREPLY=( $(compgen -W '-C -D -M -P
-Q -T -V -b -c -d -f -g -i -m -p -r -s -v' -- $cur))
else
args=0
remain=0
for (( i=1; i < COMP_CWORD; i++ )); do
case "${COMP_WORDS[i]}" in
-b|-r)
#if remain > 0
then error
remain=0
;;
-*)
#if remain > 0
then error
remain=1
;;
*)
if [ $remain
-eq 0 ]; then
args=$(($args+1))
else
remain=$(($remain-1))
fi
;;
esac
done
args=$((args-1))
case $args in
0) #LOGIC
_isabelle_logic
;;
1) #NAME
_filedir
;;
*) #END
;;
esac
fi
;;
"wwwfind")
if [[ "$cur" == -* ]]; then
COMPREPLY=( $(compgen -W '-l -c' --
$cur))
else
COMPREPLY=( $(compgen -W 'start stop
status' -- $cur))
fi
;;
*)
_filedir
;;
esac
if [[ "$cur" == -* ]]; then
COMPREPLY=( ${COMPREPLY[@]} $(compgen -W '-?' -- $cur))
fi
fi
return 0
}
complete -F _isabelle $filenames isabelle
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
