Commit a05a5f89 authored by Francois Bobot's avatar Francois Bobot

zsh : completion of theories

parent 4ce79abb
#compdef why3
##
## zsh completion for why3
## generated by ocompl
##
##
##
##
local curcontext state line cmds ret=1
local last_file
##
_arguments -s -S \
'(- *)'{-h,--help}'[Brief help message]' \
'-'"[Read the input file from stdin]"\
'*-T'"[<theory> Select <theory> in the input file or in the library]:<theory>:->theories"\
'*--theory'"[same as -T]:<theory>:->theories"\
'*-G'"[<goal> Select <goal> in the last selected theory]:<goal>:"\
'*--goal'"[same as -G]:<goal>:"\
'-C'"[<file> Read configuration from <file>]:Configuration File:_files -g '*.conf'"\
'--config'"[same as -C]:Configuration File:_files -g '*.conf'"\
"(-L --library -I)"'-L'"[<dir> Add <dir> to the library search path]:Mlpost lib path:_files -/ "\
"(-L --library -I)"'--library'"[same as -L]:Mlpost lib path:_files -/ "\
"(-L --library -I)"'-I'"[same as -L (obsolete)]:Mlpost lib path (obsolete use -L):_files -/ "\
"(-D --driver -P -prover)"'-P'"[<prover> Prove or print (with -o) the selected goals]:<prover>:->provers"\
"(-D --driver -P -prover)"'--prover'"[same as -P]:<prover>:compadd $(why3 --list-provers | egrep -E "^ [a-z]"|cut -d' ' -f 3)"\
"(-F --format)"'-F'"[<format> Input format (default: \"why\")]:<input format>:"\
"(-F --format)"'--format'"[same as -F]:<input format>:"\
"(-t --timelimit)"'-t'"[<sec> Set the prover\'s time limit (default=10, no limit=0)]:<timeout s>:"\
"(-t --timelimit)"'--timelimit'"[same as -t]:<timeout s>:"\
"(-m --memlimit)"'-m'"[<MiB> Set the prover\'s memory limit (default: no limit)]:<memory limit M>:"\
"(-m --memlimit)"'--memlimit'"[same as -m]:<memory limit M>:"\
"(-D --driver -P -prover)"'-D'"[<file> Specify a prover\'s driver (conflicts with -P)]:Prover\'s driver:_files -g '*.drv'"\
"(-D --driver -P -prover)"'--driver'"[same as -D]:Prover\'s driver:_files -g '*.drv'"\
"(-o --output)"'-o'"[<dir> Print the selected goals to separate files in <dir>]:directory output:_files -/ "\
"(-o --output)"'--output'"[same as -o]:directory output:_files -/ "\
'--print-theory'"[Print the selected theories]"\
'--print-namespace'"[Print the namespaces of selected theories]"\
'--list-transforms'"[List the registered transformations]"\
'--list-printers'"[List the registered printers]"\
'--list-provers'"[List the known provers]"\
'--list-formats'"[List the known input formats]"\
"(--type-only --parse-only -D --driver -P -prover -L --library -I -t --timelimit -m --memlimit)"'--parse-only'"[Stop after parsing]"\
"(--type-only --parse-only -D --driver -P -prover -L --library -I -t --timelimit -m --memlimit)"'--type-only'"[Stop after type checking]"\
'--debug'"[Set the debug flag]"\
'*-a'"[<transformation> Add a transformation to apply to the task]:<transformation>:->transforms"\
'*--apply-transform'"[same as -a]:<transformation>:compadd $(why3 --list-transforms | grep -e "^ ")"\
"*:The why3 file:->files"\
&& return 0
last_file=$line[-1]
case $state in
transforms)
_message "<transformations>"
compadd $(why3 --list-transforms | grep -e "^ ");
return 0
;;
provers)
_message "<provers>"
compadd $(why3 --list-provers | egrep -E "^ [a-z]"|cut -d' ' -f 3);
return 0
;;
theories)
_message "<theories of $last_file>";
compadd $(why3 --print-namespace $last_file |grep "^[a-zA-Z]" | cut -d- -f 1);
return 1;;
files)
_files -g '*.why';
return 1;;
*)
return 1
esac
#_why3 "$@"
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment