On 9/11/17, 22:20, "Norrish, Michael (Data61, Acton)" <Michael.Norrish at data61.csiro.au> wrote:

Start up with poly ?q and then emit a PolyML.print_depth 100 to get it back to printing things back to the user?

Michael

On 9/11/17, 20:42, "polyml on behalf of Timothy Bourke" <polyml-bounces at inf.ed.ac.uk on behalf of tim at tbrk.org> 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).

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