git.iko.soy/Idris-dev
on 54e4e41 help sign in
history ofsrc/Idris/Prover.hs
all commits
3cd25e6Add extra HL information to PRefDavid Raymond Christiansen a3407cbDisplay 'Hole' instead of 'Metavariable'Edwin Brady 202c913Logging levels must be explicitly mentioned.Jan de Muijnck-Hughes d2beadc7.10 compatibilityDavid Raymond Christiansen fbbe433Rename function to better reflect purposeDavid Raymond Christiansen 54cd5a6An interactive Elab shellDavid Raymond Christiansen 4dabdbaPropagate errors originating from case treesDavid Raymond Christiansen c46243bInitial implementation of semantic editor hightlightingDavid Raymond Christiansen d97715ePlumb datatype information through the proof stateDavid Raymond Christiansen c380421Move ElabTerm into Elab.TermEdwin Brady f4aaf01Guard !! in forgetEnvEdwin Brady 426d052Add provenance flag to unification errorsEdwin Brady 83793a6Add the ability for IDEs to get documentation overviewsDavid Raymond Christiansen c5de844Catch some lingering renames that I missedDavid Raymond Christiansen b85b2ebRename ideslave to ide-modeDavid Raymond Christiansen d5377beNew language-dependent FFIEdwin Brady 26da5c7Save index file when installing a packageEdwin Brady 5faaba9More information runtime error for missing caseEdwin Brady 0d8a153New way of dealing with unmatchable patternsEdwin Brady ba51147Removing matching on PSEdwin Brady 6b6aae0Avoid retrying unification problems constantlyEdwin Brady b0a0c0cImprovement for 'auto'Edwin Brady f1e161dA new primitive tactic for getting source locationsDavid Raymond Christiansen 497caf0Make output from :t name annotate with termsDavid Raymond Christiansen 705dbe1Stop encoding prover messages as outputDavid Raymond Christiansen 02e8f8cSend prover errors back with spans instead of ANSIDavid Raymond Christiansen 4fe16a5read from handle rather than stdinHannes Mehnert 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 8f7d848Don't show irrelevant MNs in proverDavid Raymond Christiansen c72d0f4Split elaborator into multiple source filesEdwin Brady 29c02f4Fix scope/matching issues in proof scriptsEdwin Brady 7d95becMake type search work in the proverDavid Raymond Christiansen c29e746Allow :doc in proverDavid Raymond Christiansen 3a2c8aaMake prover better at IDESlave protocolDavid Raymond Christiansen e363c09Better treatment of unbound implicitsEdwin Brady c201192Bring erasure info to the case tree builder.Matus Tejiscak c4eca4fMerge branch 'master' into parenthasizeInfixbmsherman 7d38943Proper and complete parenthasization of infix operator names.bmsherman e245d48Maintain pretty-printer bound varsDavid Raymond Christiansen d1a832aSend serialized versions of TT terms in pprintDavid Raymond Christiansen 7623850IDESlave protocol fixes in case of errorDavid Raymond Christiansen 2494a8aReorder code to make it more readableDavid Raymond Christiansen 387b738Remove unnecessary partialityDavid Raymond Christiansen 6d0abfbCorrect IDESlave protocol violations in proverDavid Raymond Christiansen 2d22462Check that proof steps introduce no new problemsEdwin Brady 8e55b64Show let bindings with proper line breaks and indentation in proverDavid Raymond Christiansen 9491c3cAdd ppOptionIst function.Peter Minten 5e3c248Change impl argument to a pretty printing opt recordPeter Minten bfe6499Give the pretty-printer access to info about infixesDavid Raymond Christiansen