[polyml] Poly/ML output in LaTeX

[Timothy Bourke]

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

[M***@data61.csiro.au]

On 9/11/17, 22:20, "Norrish, Michael (Data61, Acton)" <***@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-***@inf.ed.ac.uk on behalf of ***@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

[Timothy Bourke]

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

Thanks Michael.

Tim.

[David Matthews]

Post by Timothy Bourke
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
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.

Post by Timothy Bourke
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.

Post by Timothy Bourke
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.

Post by Timothy Bourke
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

[Timothy Bourke]

Post by David Matthews

Post by Timothy Bourke
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.

OK.

Post by David Matthews

Post by Timothy Bourke
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.

When I call PolyML.print_depth 0 (before a use), I see

val it = (): unit

which is not ideal, but not really a problem either since I can do all
the uses at the very beginning.

Post by David Matthews

Post by Timothy Bourke
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.

OK. I'm sorry for not seeing that before.

Post by David Matthews
Hope that answers your questions.

Perfectly. Thank you!

Tim.