On 9/11/17, 22:20, "Norrish, Michael (Data61, Acton)"
<[email protected]> 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"
<[email protected] on behalf of [email protected]> 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
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
