Open stchang opened 2 years ago
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.
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
display
doesnt seem to print unless a newline is subsequently printed after it (displayln
works fine)Example
Maybe a buffer needs explicit flushing somewhere?