Twelf should avoid long-running uninterruptable computation

[agoode]

I think we should create a new API for interfacing to twelf that lets it process a statement at a time (or perhaps an even smaller unit of processing). This will let us cleanly update the UI and do standard background processing by making twelf do work in small steps. It would also let us implement cancel.

[jcreedcmu]

A great idea. I think it'd be not too difficult to instrument the parser to return a list of document character index pairs describing where all of the top-level declarations are, and then the containing application could try loading one after the other. This would still potentially lock up the application if there were a long running %solve or the like, but I think it would take more design effort to decide out how to represent a continuation of a partially-run logic program.

A dialog with a progress bar in addition to cancel button would be good.

[jcreedcmu]

@agoode discovered the existence of a "Thread Manager" which is documented in this .sit.hqx. Not clear yet whether this is the right path, as the set of operations that are permitted for preemptable threads does not include memory allocation. Maybe instrumenting mlton compilation to add more yield points is an alternative.

[jcreedcmu]

Another @agoode find is http://www.mlton.org/MLtonSignal and http://mlton.org/MLtonThread

[agoode]

The backend support is now implemented in https://github.com/agoode/twelf/commit/ffcb3f75f96c51800d1816babef77c6772f8cf32.

The frontend has been updated to be compatible (https://github.com/jcreedcmu/twelf-mac/blob/151f33dfad011e5e9dc5491d2dc237aee96d59fa/docker/twelf-app/menus.c#L340-L344) but needs to be reworked to properly use this functionality.

[jcreedcmu]

The first thing I'm going to do is "Move twelf execution slices to idle portion of main event loop" #34

[jcreedcmu]

After that, "Implement cancellation for twelf execution" #36