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 _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
