{"push_id":732136039,"size":124,"distinct_size":0,"ref":"refs/heads/wip/tactical","head":"7a2dc7b150219b5d83aa39371af787f0c636f5cf","before":"6d7da9261878f521c5747923ab6328425814cc22","commits":[{"sha":"5f9f8b19caa45234cfbdc6999439e82e08c361b8","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Fix implicit arg / function highlights\n\nBefore, sometimes implicit args were given the FC of their function\napplication. This caused them to sometimes overwrite the highlighting\ninformation from their function when in a pattern position.","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/5f9f8b19caa45234cfbdc6999439e82e08c361b8"},{"sha":"840f5886f3b8da80fc04618bbaa6f09b46a8d5ba","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Preserve manual name type annotations\n\nThis lets highlighting code override the global state highlighting, for\nexample when emitting highlight information for something that's not yet\nin the global state.","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/840f5886f3b8da80fc04618bbaa6f09b46a8d5ba"},{"sha":"823be8699051af54ab7aedd807d18e79fa1638c1","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Highlight postulates and their definitions","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/823be8699051af54ab7aedd807d18e79fa1638c1"},{"sha":"3be8229b0365cc60f3dc4563875b20b0e1fa0bc8","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Stop overwriting case block pattern highlights\n\nThis prevents case blocks from getting their pattern clauses overwritten\nby the name of the internal auxiliary function","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/3be8229b0365cc60f3dc4563875b20b0e1fa0bc8"},{"sha":"e9e7993e4791564d427ce83cabe8e39b656eb3af","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Replace absurd syntax rule FCs\n\nPreviously, FCs coming from syntax rules would keep the FCs of their\ndefinition context. Now, after expanding a syntax rule, the FCs that\naren't contained in the region in which the syntax was expanded are\nreplaced by a reference to the present file.\n\nThis does not give a precise source location - that runs the risk of\ngenerating false highlighting information - but this solution at least\nplaces the error in the right file, and the \"While elaborating ...\" bit\ncan be used to find the error. We should probably get better at\nseparating the highlighting-relevant FCs from the\nhighlighting-irrelevant FCs in the future.","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/e9e7993e4791564d427ce83cabe8e39b656eb3af"},{"sha":"c48561f5a5945902692d01b5fcdf8e6b4e6e2e6e","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Better approximation of syntax rule errors\n\nExternal syntax is now properly used in error locations. Processing of\nhighlighting and non-highlighting FCs has been separated.","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/c48561f5a5945902692d01b5fcdf8e6b4e6e2e6e"},{"sha":"e1fce3fa2d0e3e68a8c3112ffdbc570c96a9ded7","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Fix error location in test\n\nThe syntax improvement has caused a more accurate location in an error\nin a test.","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/e1fce3fa2d0e3e68a8c3112ffdbc570c96a9ded7"},{"sha":"9107357f34eed612c253e87c24c2d8637c45036b","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Christiansen"},"message":"Merge pull request #2383 from david-christiansen/semantic-highlight\n\nFix implicit arg / function highlights","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/9107357f34eed612c253e87c24c2d8637c45036b"},{"sha":"d9d03c021fb6d5e04b4d23aba81ba3698e8500c3","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Move mention of PATH earlier in tutorial\n\nRE #2356","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/d9d03c021fb6d5e04b4d23aba81ba3698e8500c3"},{"sha":"5457da9934bf4bf561e7786ab0da812026bd6ec0","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Christiansen"},"message":"Merge pull request #2384 from david-christiansen/syntax-fc\n\nReplace absurd syntax rule FCs","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/5457da9934bf4bf561e7786ab0da812026bd6ec0"},{"sha":"8e550c1959d223f24a28cc22d71b0d05d1d189c5","author":{"email":"0b1b7393705e4755ea4dc7433b2e3d79f486e3fd@gmail.com","name":"Johannes Griebler"},"message":"Trim trailing whitespace in parseCmd\n\nWhen auto-completing a filename to :load from the REPL, the trailing\nspace added by the auto-completion will be ignored for actually loading\nthe file, but a subsequent invocation of :edit will use the path\nincluding the space, leading to the creation of a new file\n\"<module>.idr .idr\".\n\nThis problem is easily fixed by trimming not just leading, but also\ntrailing whitespace in parseCmd.","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/8e550c1959d223f24a28cc22d71b0d05d1d189c5"},{"sha":"fd5c45842166b898d4b655e55a93f70f696e4686","author":{"email":"0b1b7393705e4755ea4dc7433b2e3d79f486e3fd@gmail.com","name":"Johannes Griebler"},"message":"Simplify implementation of trim","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/fd5c45842166b898d4b655e55a93f70f696e4686"},{"sha":"1fd9722ec0af078bdca02a31addbddff8e2b7774","author":{"email":"348c32c85f2e656df5b508432d5db2052134516e@gmail.com","name":"Niklas Larsson"},"message":"Merge pull request #2387 from jgriebler/fix/repl-parse\n\nTrim trailing whitespace in parseCmd","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/1fd9722ec0af078bdca02a31addbddff8e2b7774"},{"sha":"3760508ced7d58e61a33be938444d698a877131a","author":{"email":"435e2a4f8ba8cc6bf7a8685499cd59003323ddf3@st-andrews.ac.uk","name":"Edwin Brady"},"message":"Add a timeout to checkMessages","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/3760508ced7d58e61a33be938444d698a877131a"},{"sha":"67143bdcb268a2217f2a9a3135ca1ec2c34ebb23","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Document the FFI with docstrings\n\nFixes #2381","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/67143bdcb268a2217f2a9a3135ca1ec2c34ebb23"},{"sha":"8d96041781dac1c754a7546e6f951d7bdade87d9","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Annotate links with their URL\n\nThis allows frontends other than the console to display links with a\nspecial decoration. For example, the Emacs mode underlines the link text\nand makes it clickable, and the HTML output for :printdef uses the\nappropriate tag. The console still shows the link text parenthesized\nafter the underlined link text.","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/8d96041781dac1c754a7546e6f951d7bdade87d9"},{"sha":"3275df6e230865d6e35761cf88d79e6cf596fc0f","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Add :link-href to IDE mode docs","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/3275df6e230865d6e35761cf88d79e6cf596fc0f"},{"sha":"d5c9d2336494e88a6cbb1b5f75f1b54e27d09f78","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Christiansen"},"message":"Merge pull request #2391 from david-christiansen/issue/2381\n\nBetter support for links in doc output, and docstrings for FFI","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/d5c9d2336494e88a6cbb1b5f75f1b54e27d09f78"},{"sha":"0b68452037ce98e45475e262836273201629a23c","author":{"email":"435e2a4f8ba8cc6bf7a8685499cd59003323ddf3@st-andrews.ac.uk","name":"Edwin Brady"},"message":"Added SVG logos","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/0b68452037ce98e45475e262836273201629a23c"},{"sha":"4ac4488461352b8ba44757f5933c00969d389b66","author":{"email":"a4eaabc11dc4833f27bedf2b299f4f614ec4575f@st-andrews.ac.uk","name":"Jan de Muijnck-Hughes"},"message":"Updated package documentation.\n\n+ Documented testing\n+ Documented the complete CLI for packages.","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/4ac4488461352b8ba44757f5933c00969d389b66"}]}