On 09/11/2017 08:47, Timothy Bourke wrote:

I wrote a simple LaTeX package [1,2] for exporting code snippets to validate them in an external tool and to import the resulting inferred types and error messages back into the document.

Someone contacted me about supporting Poly/ML as an external tool. To do that properly, I need to resolve three issues :

1. Suppress the "Poly/ML 5.7 Release" banner on startup while still

showing the inferred types (-q seems to suppress both).

You need "-q" to suppress the banner but then use PolyML.print_depth to control printing.

2. Import a source file without showing the inferred types (PolyML.use

seems always to show them).

Again, use PolyML.print_depth before and after you call PolyML.use.

3. Have Poly/ML terminate with a non-zero return code when an error is

found (after printing the error message).

Use --error-exit. This causes a non-zero return code on any exception including errors detected by the compiler.

Is it already possible to do such things?

If not, would it be reasonable and worthwhile to add them?

Tim.

Hope that answers your questions.

David