[Hol-info] QUse.use and exceptions

[Ramana K. <Ram...@cl...>]

Hi all,

I've noticed that the Vim mode for HOL, in particular this code:

https://github.com/HOL-Theorem-Prover/HOL/blob/master/tools/vim/vimhol.src#L57

has occasionally stopped passing back raised exceptions to the REPL.
>From the UI perspective, this means the user gets no feedback when a
command fails (it appears as if nothing happened). I believe this
change probably happened after the switch from Poly/ML's native use to
QUse.use.

Looking at QUse, I notice that it calls the Poly/ML compiler function like this:

https://github.com/HOL-Theorem-Prover/HOL/blob/master/tools-poly/poly/quse.sml#L59

Does anyone know whether this is going to have the same
exception-raising behaviour as the native use function, or if it is
indeed the culprit? Are there compiler flags or something else that
could be passed to get the correct handling of exceptions?

Cheers,
Ramana