git.iko.soy/Idris-dev
on d773edd help sign in
history ofsrc/Idris/Interactive.hs
all commits
3ccb494Remove the empty property 'copyright'.Jan de Muijnck-Hughes 4a3fe0cLinearTypes extension improvementsEdwin Brady 83bb62fUnused binds (#4067)Jason Felice 608fbddAdd function for strictly reading sourceNiklas Larsson 3eabd63Fix problems when adding missing clausesMatthias Heinzel a463bb1Collected language PRAGMAs and removed debugging commentsAhmad Salim Al-Sibahi fb33d8cIndentation configuration via command line args.Steven Shaw e1c210bAdd 'RigCount' to Pi and PVarEdwin Brady e6ceb5cAlphabetize and indent imports and LANGUAGE pragmasEcho Nolan 0df1270Change Instance to implementation (#3404)(λ _ λ) 06d9db6Use interface instead class or type class in documentations (#3379)(λ _ λ) c3f0755replace code level class symbol with inferfacezjhmale 08cef17HLint DIrected Code CleanupJan de Muijnck-Hughes 72a6169Display of lifted typesEdwin Brady fdfa04cStore file with constraints + exportEdwin Brady 0896073Added documentation for modules.Jan de Muijnck-Hughes 7412545New line after with in interactive modeEdwin Brady be0ff0fAdd 'definable' flag to metavariablesEdwin Brady 930f8acmakeLemma heuristic for when to show classesEdwin Brady 1909c32Moved Quasiquote under Elab namespace.Jan de Muijnck-Hughes fbd940cFix bracketing when solving holes interactivelyEdwin Brady 6eaf933Disambiguation tweakEdwin Brady 467490bBetter case split when all patterns are impossibleEdwin Brady db07875Merge "add definition" and "add missing" commandsEdwin Brady 55ffc21Some display tweaks for explicit argumentsEdwin Brady 1e80f1fNo newline after case in :makecaseEdwin Brady 0140e67Tweak to hole liftingEdwin Brady 96e9b1aVariable names in makelemma typesEdwin Brady 7095d6cProof search should only use user visible namesEdwin Brady 0f80f56Don't want newline after makeCaseEdwin Brady 5bd5777Add :makecase (:mc) to REPL and ide-modeEdwin Brady b49c2fdBetter display of classes in makeLemmaEdwin Brady 3cd25e6Add extra HL information to PRefDavid Raymond Christiansen 202c913Logging levels must be explicitly mentioned.Jan de Muijnck-Hughes 7dca9b4Minor rewording of error messageEdwin Brady a0b9687Don't crash on :addmissing for defns with no clausesDavid Raymond Christiansen 0419a12Highlight let bindingsDavid Raymond Christiansen 689e64bHighlight pi and lambda bindersDavid Raymond Christiansen c380421Move ElabTerm into Elab.TermEdwin Brady f987aecAdd info field to AppEdwin Brady 4dd164cSet encoding for read files.Niklas Larsson b85b2ebRename ideslave to ide-modeDavid Raymond Christiansen 17fe233Add scoped implicit argument to PiEdwin Brady e95c877Make pattern matching consistent in lambda/letEdwin Brady 3ade599Partial evaluator fixesEdwin Brady 7e7368dStore kind in Pi bindersEdwin Brady 86b60b2Take .lidr syntax into account with :addmissingDavid Raymond Christiansen 480024cRemove all the handle argumentsDavid Raymond Christiansen 1add7b7provide a Handle for IdeSlave, used to read from and write to (instead of hardcoded stdin/stdout) also send protocol-version message when the client connects also accept a single client connection when --ideslave-socket is provided (I don't see any reason to have multiple clients at all!)Hannes Mehnert c72d0f4Split elaborator into multiple source filesEdwin Brady