Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2015-RC0 ML ATP_Util.unyxml

Email Gateway (Aug 22 2022 at 09:09):

From: "C. Diekmann" <diekmann@in.tum.de>
Dear 2015-RC0 ML folks,

I'm looking for a replacement of the ATP_Util.unyxml ML function. I
was using it the following:

ML{*
fun term_to_string (ctx: Proof.context) (n: term) : string =
n |> Syntax.pretty_term ctx |> Pretty.string_of |> ATP_Util.unyxml
*}

Cornelius

Email Gateway (Aug 22 2022 at 09:10):

From: Makarius <makarius@sketis.net>
On Mon, 13 Apr 2015, C. Diekmann wrote:

I'm looking for a replacement of the ATP_Util.unyxml ML function. I
was using it the following:

This is now called YXML.content_of.

ML{*
fun term_to_string (ctx: Proof.context) (n: term) : string =
n |> Syntax.pretty_term ctx |> Pretty.string_of |> ATP_Util.unyxml
*}

Here is a more canonical version of the above, using standard Isabelle/ML
idioms:

ML ‹
fun term_to_string ctxt t =
Syntax.pretty_term ctxt t |> Pretty.string_of |> YXML.content_of
›

Types carry a priori no meaning in ML, especially the main types of the
LCF framework. Above Proof.context, term, and also string don't say
anything specific about what you give in an get out (the string it is
essentially a markup tree). The language is semantically untyped in this
respect.

Instead, you use canonical names for what you mean: proper spelling of
"ctxt" is especially important. In the "implementation" manual section
0.1.2 there are more hints on professional usage of names in Isabelle/ML.

Makarius

Last updated: Apr 26 2024 at 16:20 UTC