You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The buffer that needs 'explicit flushing' is NewlineFlushingOutputPort in runtime/core/ports.js.
Thought about this a little bit and the solutions that come to mind are non-trivial. node offers process callbacks, so server-side you could write
process.on('exit',()=>flushCurrentOutputPort())
But process isn't available in the browser. We could write a 'cleanup' function that flushes all output ports and registers/deregisters ports as current-output-port is modified or other ports are constructed, but that adds some overhead to all programs. Other option is to stop buffering altogether, but not sure if that's desired behavior.
Activity
gamburgm commentedon Jan 10, 2022
The buffer that needs 'explicit flushing' is
NewlineFlushingOutputPortinruntime/core/ports.js.Thought about this a little bit and the solutions that come to mind are non-trivial.
nodeoffersprocesscallbacks, so server-side you could writeBut
processisn't available in the browser. We could write a 'cleanup' function that flushes all output ports and registers/deregisters ports ascurrent-output-portis modified or other ports are constructed, but that adds some overhead to all programs. Other option is to stop buffering altogether, but not sure if that's desired behavior.stchang commentedon Jan 10, 2022
Thanks for thinking about this! I thought it would be an easy fix but then I looked into it for a while and couldnt figure it out.
I think the argument has to be a buffer so that in the future we could possibly support the entire port api if we wanted