Been doing a bit of thinking about how to lash the editor and the elaborator together without being too specific about how it’s actually got to work. I reckon the elaborator provides something like
subscribe :: (Response → IO ()) → IO (Request → IO ())
where Response and Request are part of the interface—types of signals from and to the elaborator.
Editors thus explain how they listen and are taught in return how to ask. There is no other way to get a straight answer from the elaborator. Stuff happens, as and when. An ‘editor’ might serve merely to write Responses to stdio and read Requests from stdin.
There is also no reason why multiple editors should not simultaneously subscribe (corresponding either to having multiple users, or to visiting multiple files). The elaborator should broadcast updates to all subscribers, but should respond privately to requests for information. Update responses will carry the name of what’s being updated, so the listener which an editor sends may perfectly well filter out uninteresting responses server-side.
Carry on like this and we’ll be doing eScience!