git.iko.soy/Idris-dev
on d66da21 help sign in
history ofsrc/Idris/Completion.hs
all commits
cc9acdaAdd 'equiv' to autocompletion of tacticsEdwin Brady 01078f2Merge pull request #641 from ahmadsalim/feature/metavarprooffixEdwin Brady 1e6c727Disallow proving of top-level declarations and other meta-variables, fixes idris-lang/Idris-dev#46Ahmad Salim Al-Sibahi 8e974c7Parser cleanup. Removing scaffolding parsers, rewrite PParser and IdeSlave from parsec to Haskell. No more parsec dependenciesAhmad Salim Al-Sibahi 91317fbAdd new editor commands to tab completionDavid Christiansen f34f0afBetter display of metavariable types in :tEdwin Brady 583cc43Add ability to set ANSI italicsDavid Christiansen 1085d22Tab completion for setting colours at the REPLDavid Christiansen c404489Add primitive vector types to REPL autocompletionBenjamin Saunders f540cf5remove duplicate 'intro' and 'intros'Hannes Mehnert c7fded1Added 'mrefine' tactic Like refine, but uses matching instead of unification to resolve implicit arguments. All will become clear, I hope :). This is intended for an additional style of pattern matching (on types) for better explanation of proofs.Edwin Brady 25ae311Add primitive type names to name completionDavid Christiansen c1a4eacFull TT reflection and reificationJan Bessai a029bd8reduce duplication by providing a show instance for CmdArgHannes Mehnert 2297270unify help and completion of REPL - previously they were not in sync, now it is one lookup tableHannes Mehnert 1617dd3Stop completion of names that are prefixes of othersDavid Christiansen 25a4649Only use metavariables as completions for :p and :proveDavid Christiansen 0bcdd51Complete identifiers following non-whitespaceDavid Christiansen 1e86384Haddock for completion moduleDavid Christiansen 66d8360Crude support for completion in proverDavid Christiansen 52203a3Complete tactic names in proverDavid Christiansen cc80288Rename the REPL's Haskeline uses to make them obviously REPL-specificDavid Christiansen cc3c913Complete arguments of commands (though slightly crudely)David Christiansen f0e096bComplete multiple identifiers in one expressionDavid Christiansen fc58a50Simple completion supportDavid Christiansen