on 4e4b7df help sign in
all commits
60b43b4Add raw name quotesDavid Raymond Christiansen c9c3bfaSemantic highlighting of implicit fromIntegerDavid Raymond Christiansen bc2915cMerge remote-tracking branch 'upstream/master' into parser-highlightsDavid Raymond Christiansen 5da0d60Faster processing of alternativesEdwin Brady a54852bHighlighting for pairs, lists and sigmasDavid Raymond Christiansen 3cd25e6Add extra HL information to PRefDavid Raymond Christiansen 09f56a7Add compiler highlighting for quoted names in sourceDavid Raymond Christiansen cb1805bAdd local namespace access to ElabDavid Raymond Christiansen 64ab360Tracking and highlighting of metavariablesDavid Raymond Christiansen 7e8e25bMerge branch 'master' into name-highlightsDavid Raymond Christiansen 0419a12Highlight let bindingsDavid Raymond Christiansen f3fef7ePrecise tracking of bindings in do blocksDavid Raymond Christiansen 53e1281Remove PEqMelvar Chen 8984d49Remove PRefl and all references to itMelvar Chen 689e64bHighlight pi and lambda bindersDavid Raymond Christiansen c46243bInitial implementation of semantic editor hightlightingDavid Raymond Christiansen 90127b3High-level if ... then ... else ... expressionDavid Raymond Christiansen 688f324Use any instead of or/map and null/filterNiklas Larsson 8ab1ac6Richer universe error objectsDavid Raymond Christiansen 66c9c38Report universe errors using IDE protocolDavid Raymond Christiansen d6458bbAdd `{n} for quotations of the global name nDavid Raymond Christiansen c3def79Rename Tactical to ElabDavid Raymond Christiansen 933fcbbAdd missing cases to warnDisambDavid Raymond Christiansen d745c2eMerge pull request #1852 from 4e6/repl-module-reloadEdwin Brady 60e4921Relax lower bound on mtlEric Mertens 39c07a7Proper REPL module reloadingDmitry Bushev 2e6b5e0Fix universe checking errorEdwin Brady 73bad9fAdd missing pattern in warnDisambEdwin Brady e95c877Make pattern matching consistent in lambda/letEdwin Brady 684a578Completely replace ErrorT with ExceptTbmsherman edb9980Removed '_|_' as a built in declaration and renamed it to 'Void', 'FalseElim' now 'VoidElim' to match upAhmad Salim Al-Sibahi ce7dff9Error when using empty namespace for disambiguation at REPLDavid Raymond Christiansen 480024cRemove all the handle argumentsDavid Raymond Christiansen 019c98aFix missing function call from 723d972b2David Raymond Christiansen 723d972Fix IDESlave reporting of ProofSearchFailDavid Raymond Christiansen f0a5442Provide IDESlave output with docs and typeDavid Raymond Christiansen fb3f7f0Use At to hold FCsDavid Raymond Christiansen aed179cTrack the providence of unification errorsDavid Raymond Christiansen 7437ebePrepared data structure of FC for spanning, and added the span of the last token parsed to IdrisAhmad Salim Al-Sibahi 5987a95Report errors loading files using semantic highlightingDavid Raymond Christiansen 0c8c90dStrictness annotationsEdwin Brady 40da42fSupport names and terms in error reflectionDavid Raymond Christiansen b0e43f0Initial partial version of REPL error reflectionDavid Raymond Christiansen 5000aebAdd a Cabal libraryBrian McKenna b1537b9Report errors directly, instead of parsing the string given to ihputStrLnHannes Mehnert 3c32b65Whitespace cleanup.George Leontiev 57c8657Added column name to sourceAhmad Salim Al-Sibahi 53b28e6Update compiler to use new error handlingDavid Christiansen ac33945Wrap Idris in an ErrorTDavid Christiansen 66ff954Make the type of ierror more generalDavid Christiansen