git.iko.soy/Idris-dev
on 7afa310 help sign in
history ofsrc/Idris/Completion.hs
all commits
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 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