[isabelle-dev] Bash subcommand completion for isabelle

[Mathieu Giorgino]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110926/299a1f39/attachment-0002.html>
-------------- next part --------------
# vim: set ft=sh ts=2 sw=2 et:
# file: /etc/bash_completion.d/isabelle

# Bash completion for isabelle
# Original: Mathieu Giorgino <Mathieu.Giorgino at gmail.com>
#
# 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