Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.Interaction.Options.BashCompletion
Description
Tools for shell completion scripts.
Bash completion takes a list of completion words (the current commandline) and a completion index (the current word to be completed) and returns a list of possible completions of this word.
To do bash completion inside Agda, we need to pass this data to Agda.
So we equip Agda with a special option --bash-completion
which takes
first the completion index (number) and then the completion words.
E.g.
agda --bash-completion 1 --warn
This should complete --warn
to --warning=
.
agda --bash-completion 1 --warning=
This would list the possible values for WARNING. However, these are too many and one may get the annoying question whether one really wants to see all. So we should only produce a small enough list. We show the common prefixes of all values up to a maximal number (threshold). To this end, we may store the possible completion as a compressed trie where instead of letters we use maximal non-overlapping prefixes. Then we compute a fair truncation of the tree so that the total number of leaves stay below the threshold.
Synopsis
- type Help = String
- printedOptions :: [String]
- printedOptionsWithHelp :: [(String, Help)]
- printOptions :: [OptDescr a] -> [(String, Help)]
- type Truncate = Maybe Int
- bashComplete :: Truncate -> [String] -> Either String String
- data Completion = Completion {}
- optionsTrie :: Trie Char Help
- complete :: Truncate -> String -> Completion
Documentation
printedOptions :: [String] Source #
printedOptionsWithHelp :: [(String, Help)] Source #
printOptions :: [OptDescr a] -> [(String, Help)] Source #
Print just the names of the given options (e.g. for bash completion scripts). For long options with finitely enumerable arguments, print all variants.
type Truncate = Maybe Int Source #
Should the completions
be truncated to a given maximum number of prefixes?
Arguments
:: Truncate | Truncate completions suggestions? To how many? |
-> [String] | Arguments following |
-> Either String String | Error or |
Handle the option --bash-complete
.
It expects the index COMP_CWORD
as first argument
that tells which of the following arguments COMP_WORDS
is supposed to be completed.
It either returns an error message or the result for COMPREPLY
.