git.iko.soy/Idris-dev
on 1b71663 help sign in
history ofsrc/Idris/Core/Execute.hs
all commits
56c2058Make binary files the default when opening.Niklas Larsson 3ccb494Remove the empty property 'copyright'.Jan de Muijnck-Hughes 4a3fe0cLinearTypes extension improvementsEdwin Brady 83bb62fUnused binds (#4067)Jason Felice d4bd8e6Clean up unused imports (#4065)Jason Felice a521cc4Fix the idris_time special case.Chris Ford 4317228Handle idris_mkFileError through a special-case.Chris Ford 6e09d8fFlush output buffers in executorDavid Raymond Christiansen 2debf36Use offset for substr if possibleEdwin Brady ce5e330Add StringBuffer to Prelude.StringsEdwin Brady fb185aaCheck for linearity of constructorsEdwin Brady a5033e7Add linear LamEdwin Brady e1c210bAdd 'RigCount' to Pi and PVarEdwin Brady e3daf28Add RigCount to environmentEdwin Brady ea88b5eBetter choice of pattern to inspect in coverageEdwin Brady 521b8bfRemove unused case tree codeEdwin Brady 20d4426this command will be translated into a call `hSetBuffering` or `setvbuf` to disable buffering in stdin/stdoutCarsten König e6ceb5cAlphabetize and indent imports and LANGUAGE pragmasEcho Nolan f754d9cPurify Idris of "return"David Christiansen 3285207Check file size before reading in readFileEdwin Brady 0896073Added documentation for modules.Jan de Muijnck-Hughes b1872fbFile IO type indicates possibility of failureEdwin Brady 7095d6cProof search should only use user visible namesEdwin Brady f987aecAdd info field to AppEdwin Brady fc02362Support externally defined primitivesEdwin Brady 13ebfcfFix partiality in executor and give better errorDavid Raymond Christiansen 39e4eb0IO primitives tweak to support JSEdwin Brady f6df58cMerge branch 'master' of github.com:idris-lang/Idris-dev into new_ffiEdwin Brady 9150698Primitive type for world stateEdwin Brady d5377beNew language-dependent FFIEdwin Brady 60e4921Relax lower bound on mtlEric Mertens 10d5903Add emulation of getchar to executorDavid Raymond Christiansen 17fe233Add scoped implicit argument to PiEdwin Brady a4401f9Import ExceptT type and constructorBen Sherman 1728a65Disambiguate forM callbmsherman 684a578Completely replace ErrorT with ExceptTbmsherman 00f1cd5Use ExceptT instead of ErrorTbmsherman 6359d99Removed dead code and lifedt TODO/FIXME from Core/Execute.Jan de Muijnck-Hughes 0200b44Support uniqueness types when executing IO actions in REPLMort Yao e7bd1f5Uniquify binder names when leaving executorDavid Raymond Christiansen 7e7368dStore kind in Pi bindersEdwin Brady e30ff97Merge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady b0e53f8Support the RTS function idris_time in executorDavid Raymond Christiansen b7316b7Better errors from executorDavid Raymond Christiansen 09e5383Require that arguments to case blocks be reducedDavid Raymond Christiansen 2aaff41Stop erasing binder types in executorDavid Raymond Christiansen 51a9b69Open files in binary modeDavid Raymond Christiansen 218c735Mark 'case' on unique types as updatableEdwin Brady 9abbc3fCache uniqueness information in NameTypeEdwin Brady 6250eb4Make executor emulate putcharDavid Raymond Christiansen