This PR replaces the CodeMirror interactions window with a proper terminal editor. This branch mostly works, and is missing the following minor features:
Proper Ctrl-D behaviour -- it's supposed to flush the linebuffer, not kill all input, but what we have is good enough for now.
This PR replaces the CodeMirror interactions window with a proper terminal editor. This branch mostly works, and is missing the following minor features:
This fixes #444.