git.iko.soy/Idris-dev
on aeb032a help sign in
history ofsrc/Idris/Completion.hs
all commits
83bb62fUnused binds (#4067)Jason Felice 8f6f9afCode style tweakSteven Shaw 6e66041Tweak for stylish-haskellSteven Shaw 5950e1ePrevent private functions showing up in autocomplete and :t.Steven Shaw d4ce631Add :! for running shell commands from the REPLRyan Scott e6ceb5cAlphabetize and indent imports and LANGUAGE pragmasEcho Nolan 56ecebfREPL improvementsBartosz Przygoda 08cef17HLint DIrected Code CleanupJan de Muijnck-Hughes c6f1061Remove vestiges of pre-SpecialName namesMelvar Chen 0896073Added documentation for modules.Jan de Muijnck-Hughes be0ff0fAdd 'definable' flag to metavariablesEdwin Brady e95b013Made Parser submodules actual submodules.Jan de Muijnck-Hughes c292d12Moved REPLParser to be under REPL namespace.Jan de Muijnck-Hughes ce35f7aKeep :set options in sync.Robert Clipsham 81a73e9Add desugarnats to completionNiklas Larsson 7095d6cProof search should only use user visible namesEdwin Brady effc954Add function to list installed packagesBen Sherman d31f30fDefault to no REPL completion if not yet implementedBen Sherman 99be9f0Various cleanup of the REPL, mainly with parsing and completionBen Sherman 3c475f4Improve REPL completion and DRY in parsing/completionBen Sherman 36e304dLifted TODO/FIXME issues to the issue tracker.Jan de Muijnck-Hughes f1e161dA new primitive tactic for getting source locationsDavid Raymond Christiansen ae1aed9Add completion support for newer command arg typesDavid Raymond Christiansen e91819cFinal cleanup/check of case tactic implementationAhmad Salim Al-Sibahi 47304d9Allow the big startup banner to be disabledDavid Raymond Christiansen 51394aaAdd 'unify' tacticEdwin Brady ecd8c56Make completeCmd totalBrian McKenna 423b4c4Allow users to disable the auto-solve in the proverDavid Raymond Christiansen c37de47Propagate parameters to recordsEdwin Brady af0171eProver commands for evaluation and typechecking expressionsDavid Raymond Christiansen 4257d64Automatically detect console widthDavid Raymond Christiansen b8d7935Hide original errors upon reflective rewriteDavid Raymond Christiansen 46e894dUse Data.Text for variable namesEdwin Brady f793c7bAdd tab completion for "induction" in proverDavid Raymond Christiansen 53b84ecMerge branch 'cabal-library' of https://github.com/puffnfresh/Idris-dev into puffnfresh-cabal-libraryEdwin Brady 5e7fc5dAdd 'byReflection' tacticEdwin Brady 67da31aMerge branch 'master' into cabal-libraryBrian McKenna cc9acdaAdd 'equiv' to autocompletion of tacticsEdwin Brady 5000aebAdd a Cabal libraryBrian McKenna 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