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).
2. Import a source file without showing the inferred types (PolyML.use seems always to show them).
3. Have Poly/ML terminate with a non-zero return code when an error is found (after printing the error message).
Is it already possible to do such things?
If not, would it be reasonable and worthwhile to add them?
Tim.
[1]: http://www.ctan.org/pkg/checklistings [2]: https://github.com/tbrk/checklistings