feature request: go to location when "F*: subprocess exited".

[fournet]

I often make syntax errors. I get F*: subprocess exited on the command line, and go to the Messages buffer to know where to look at:

[F* raw output] Interactive mode; ignoring --verify_module{"kind":"protocol-info","version":1,"features":["autocomplete","describe-protocol","exit","lookup","lookup/documentation","pop","push"]}
[F* error] C:/cygwin64/home/fournet/everest/mitls-fstar/src/tls/Handshake.fst(310,18-310,18): (Error) Syntax error: Parsing.Parse_error
[F* error] 1 error was reported (see above)
F*: subprocess exited.
Mark set [2 times]

Displaying the detailed error within my fstar buffer would be very convenient.

[cpitclaudel]

Yeah, it's a pain. But it would be much better if F* simply didn't die (and instead reported a regular error). See FStarLang/FStar#912 for the F* side.