on 7afa310 help sign in
all commits
cb5ed53Added TODOs from IdeSlave.hsJan de Muijnck-Hughes fe8927cIDE support for :printdefDavid Raymond Christiansen 7ce4d90Add annotations for :search result classificationbmsherman a0ccc57move getNChar and getLen to IdeSlaveHannes 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 e245d48Maintain pretty-printer bound varsDavid Raymond Christiansen f50b357Add commands for working with serialised termsDavid Raymond Christiansen d1a832aSend serialized versions of TT terms in pprintDavid Raymond Christiansen d6c5b2bAdd semantic highlighting for postulatesDavid Raymond Christiansen 94fc13cIDESlave support for :loadtoDavid Raymond Christiansen f8759cdIDESlave support for setting the depth of interactive proof searchDavid Raymond Christiansen 659e985Add IDESlave support to :makelemmaDavid Raymond Christiansen e16c068Documentation for primitivesDavid Raymond Christiansen 89a975eImprove ideslave highlighting of primitivesDavid Raymond Christiansen 65e2aa7Add support for :refine to IDESlaveDavid Raymond Christiansen e07c13dAdd :refine (:ref) command for refining a holeEdwin Brady 39e4022Simplify protocol to IDESlave and :who-calls, :calls-whoDavid Raymond Christiansen 418a6b6Add :who-calls and :calls-who to IDESlaveDavid Raymond Christiansen e3cfa93Add command to IDESlave for metavarsDavid Raymond Christiansen f0a5442Provide IDESlave output with docs and typeDavid Raymond Christiansen dd20facAdd semantic highlighting info for metavariablesDavid Raymond Christiansen 8325cedAllow getting and setting options from IDESlaveDavid Raymond Christiansen e9ef380Support text formatting in docstringsDavid Raymond Christiansen 1b81d69Merge pull request #985 from david-christiansen/keyword-highlightEdwin Brady 15aebc9Add highlighting for keywords in interpreter outputDavid Raymond Christiansen bb3a7b7Support :apropos in IDESlaveDavid Raymond Christiansen 7437ebePrepared data structure of FC for spanning, and added the span of the last token parsed to IdrisAhmad Salim Al-Sibahi 6370ef3Add missing output annotation serialization to ideslaveDavid Raymond Christiansen 71b477bAdd IDESlave command for getting documentationDavid Raymond Christiansen 5987a95Report errors loading files using semantic highlightingDavid Raymond Christiansen 4d2185bSupport semantic highlighting in IDEslave modeDavid Raymond Christiansen 67da31aMerge branch 'master' into cabal-libraryBrian McKenna cbe9965on error, report the column, as well as the line number in the ideslave mode.Hannes Mehnert 5000aebAdd a Cabal libraryBrian McKenna 8e974c7Parser cleanup. Removing scaffolding parsers, rewrite PParser and IdeSlave from parsec to Haskell. No more parsec dependenciesAhmad Salim Al-Sibahi 6fb995dsupport for add-proof-clause in IdeSlaveHannes Mehnert f6edbf0support for add-missing, make-with-block and proofsearch for ideslaveHannes Mehnert dbe880csupport for add-clause in IdeSlaveHannes Mehnert 40611beImplement CaseSplit in IdeSlaveHannes Mehnert 6412ae4Implement type-of ideslave command, which uses Check in the backgroundHannes Mehnert f18d79cRemove calls to "error". Fixes #607.David Christiansen 9b4b7dccleanupsHannes Mehnert 1721a22more work on the prove mode... now sending messages when it started and finishedHannes Mehnert b9df272layout improvementHannes Mehnert 9505a71cleanups, rename List to SexpList to disambiguateHannes Mehnert 674c8b8IdeSlave mode improvements: - introduce iResult and iFail to report success and failure of a REPLcommand - send warnings for occuring warnings during parsing / typechecking - introduce ideslaveProcess function, which guards process with iResult/iFail (and does not support all operations) - revert commit which removed IState from ideslaveStart/ideslave functionsHannes Mehnert 2253212send prompt over the wire - also minor refactoringHannes Mehnert d2e1c8cfix parsing of escaped quotes inside of stringsHannes Mehnert 4118b79implement outputmode in IState, which either prints it raw or sexpressions (for ideslave support)Hannes Mehnert