summaryrefslogtreecommitdiff
path: root/src/interactive.ml
AgeCommit message (Collapse)Author
2019-10-25Allow interactive commands to be setup outside isail.mlAlasdair Armstrong
can use Interactive.register_command to set up a new interactive command, which allows commands to be set up near where the functionality they interact with is defined, e.g. the ast slicing commands are registered in Slice.ml. Also allows help messages to be generated in a consistent way.
2019-02-06Improve emacs modeAlasdair Armstrong
Can now use C-c C-s to start an interactive Sail process, C-c C-l to load a file, and C-c C-q to kill the sail process. Type errors are highlighted in the emacs buffer (like with merlin for OCaml) with a tooltip for the type-error, as well as being displayed in the minibuffer. Need to add a C-c C-x command like merlin to jump to the error, and figure out how to handle multiple files nicely, as well as hooking the save function like tuareg/merlin, but this is already enough to make working with small examples quite a bit more pleasant.
2018-12-22Improve error messages and debuggingAlasdair Armstrong
Work on improving the formatting and quality of error messages When sail is invoked with sail -i, any type errors now drop the user down to the interactive prompt, with the interactive environment being the environment at the point the type error occurred, this means the typechecker state can be interactively queried in the interpreter to help diagnose type errors.