edwinb/Idris-dev — pull request #312 by hannesm (2013-05-11 19:17:46+00:00)
Title: Ideslave option

For further improvements of the emacs mode of idris (and any other editor mode), I developed a protocol so that we do not need to screen scrape the output of idris.

The wire protocol is as following: first 6 characters which contain the length of the message, encoded in hexadecimal (0-prepended). Afterwards the actual command is given, as a s-expression - meaning a list containing the command as first element, arguments are following and the last element is an identifer - chosen by the editor, and preserved by idris (``IState - idris_outputmode - IdeSlave Integer``). Thus, for every message the request can be matched.

The commands from the editor to idris are at the moment limited to:
* ``interpret`` which interprets the following string (similar to the repl)
* ``repl-completions`` which returns the completions for the given prefix
* ``load-file`` which loads the given file

The commands from idris to the editor vary a bit more:
* ``return (ok result)`` command was successfull, result is in result
* ``return (error condition)`` command resulted in an error, message is in condition
* ``write-string msg`` output (for debugging, etc)
* ``set-prompt prompt`` prompt changed (loaded modules changed)
* ``warning (filename line-number message)`` warning occured in the given file at the given line number

A more complete documentation of the protocol will follow. An implementation for the editor side is available from https://github.com/hannesm/Idris-mode/tree/ideslave

Currently there are some limitations:
* logging is not supported
* execute does not work
* proof mode is not supported yet

I'm happy to work on further features, but would also be happy to get this pull request in (or get feedback what I should not do in Haskell code ;).