Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Syntax.string_of_term changed in Isabelle2013

Email Gateway (Aug 19 2022 at 11:35):

From: Walther Neuper <wneuper@ist.tugraz.at>
In Isabelle2012 the function

fun term_to_str t = Print_Mode.setmp [] (Syntax.string_of_term
(Proof_Context.init_global (Thy_Info.get_theory "Isac"))) t;

term_to_string @{term "a+1::int"}

delivered

"a+1": string

which we need for checks in our test suite.

In Isabelle2013 the respective functions in "Syntax" deliver strings
apparently for the fontend ( "<markup> ..."). Where do we get a
(combination of) function(s) with signature

: _ -> term -> string

in Isabelle2013 ?

PS: We cound't find an answer neither in isar-ref.pdf "7.1.Printing
logical entities" nor in implementation.pdf "3.2.Parsing and unparsing"
(the FIXME might concern our question --- nevertheless, thanks for the
ever-increasing quality of the manuals !!!).

Email Gateway (Aug 19 2022 at 11:35):

From: Makarius <makarius@sketis.net>
Here is an example that works better:

ML {*
fun term_to_string ctxt t =
let
val ctxt' = Config.put show_markup false ctxt;
in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;

term_to_string (Proof_Context.init_global @{theory Main}) @{term "a+1::int"}
*}

Note that show_markup is the key thing here. You should also avoid
Thy_Info.get_theory, since it only works in certain situations (theory
produced TTY or batch mode).

What are you doing with the string output anyway? It is relatively hard
to rely on exact behaviour of inner syntax layers, apart from the normal
mode of operation as user input / output.

Makarius

Email Gateway (Aug 19 2022 at 11:35):

From: Walther Neuper <wneuper@ist.tugraz.at>
On 07/21/2013 11:03 AM, Makarius wrote:

On Sat, 20 Jul 2013, Walther Neuper wrote:

In Isabelle2012 the function

fun term_to_str t = Print_Mode.setmp [] (Syntax.string_of_term
(Proof_Context.init_global (Thy_Info.get_theory "Isac"))) t;
:
in Isabelle2013 ?

Here is an example that works better:

ML {*
fun term_to_string ctxt t =
let
val ctxt' = Config.put show_markup false ctxt;
in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;

term_to_string (Proof_Context.init_global @{theory Main}) @{term
"a+1::int"}
*}

Note that show_markup is the key thing here. You should also avoid
Thy_Info.get_theory, since it only works in certain situations (theory
produced TTY or batch mode).

Thanks a lot for the function (we got stuck with Pretty.T) and the note ...

What are you doing with the string output anyway? It is relatively
hard to rely on exact behaviour of inner syntax layers, apart from the
normal mode of operation as user input / output.

... because a considerable part of our regression tests still uses this
function.

We shall narrow the gap to Isabelle standards also in isac's test
configuration, but that will take time (and won't start before all tests
are running on Isabelle2013 ;-)

Walther

Last updated: Apr 26 2024 at 04:17 UTC