git.iko.soy/Idris-dev
on ff7ea9d help sign in
history ofsrc/Idris/Interactive.hs
all commits
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 6cc18fdmakelemma fixEdwin Brady e363c09Better treatment of unbound implicitsEdwin Brady 9907240Add new Err constructor to disambiguate the CantResolveAlts constructor.bmsherman f8759cdIDESlave support for setting the depth of interactive proof searchDavid Raymond Christiansen 094be98Add an optional depth to 'search' tacticEdwin Brady 659e985Add IDESlave support to :makelemmaDavid Raymond Christiansen a265279:makelemma now works on provisional definitionsEdwin Brady 719d472'search' now fails if there are metavariablesEdwin Brady 50f63b5Make sensible implicit choices in :addlemmaEdwin Brady f8e6549:addclause now adds template bodies to instancesEdwin Brady db88c3eTidy output of :makelemmaEdwin Brady af99a9dAdd :makelemma command in interactive editingEdwin Brady