Emacs mode

The Emacs mode is called, unsurprisingly, esml-mode. You can get it by running package-install-file on the esml-mode.el file, in the emacs subdirectory. The mode provides some syntax highlighting (courtesy of sml-mode), and functionality to communicate with the repl. The functions are as follows:

• \C-c \C-i — start the repl / jump to the repl buffer (since I'm a lousy elisp hacker, you have to run this before loading a file)
• \C-c \C-l — load a file into the repl. If successful, this locks the buffer, leaving only the holes open for free editing.
• \C-c \C-n — focus on the next hole. Next means the hole after the currently focused one, or, if no focus is present, after the point. This also displays the context of the hole in a buffer.
• \C-c \C-p — focus on the previous hole (previous in the analogous sense to next above).
• \C-c \C-r — "refine" the focused hole. The simplest form of working with a hole, this function takes the content of the focused hole, typechecks it in the appropriate context and — provided the typechecking succeeded — fills the hole with the content. Note, the contents of the hole can be any valid term, in particular new holes.
• \C-c \C-a — "apply" the focused hole. Slightly similar to refine, this function takes the content of the hole and checks if its type ends in the type of the hole, i.e., if a valid refinement of the hole is an application of a given term to some number of arguments. If so, it refines the hole with the given term applied to an appropriate number of new holes.
• \C-c \C-s — "split" the focused hole. This function takes the contents of the hole, and performs a case-split on them. The term in the hole gets type-checked and, provided its type is an algebraic datatype, the hole is filled with an exhaustive case expression, matching the contents of the hole, and with a new hole in each branch. The naming of the variables could use some sophistication, I know, but that's future work.