Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] updating code that calls add_locale_i


view this post on Zulip Email Gateway (Aug 18 2022 at 14:41):

From: Michael Norrish <Michael.Norrish@nicta.com.au>
My old code included:

Locale.add_locale_i (SOME "")
localename
(Locale.Locale globloc)
[e']
thy

What should I do now that the nearest equivalent seems to be
Expression.add_locale? The type of the latter is a bit confusing. In
particular, the equivalent of the (Locale.Locale globloc) looks as if
it should be a expression_i, but such expressions have to include a
term if they are to convey any useful information at all, and it's
unclear to me quite what that term should be.

Or is Expression.add_locale not the right thing to be calling?

Michael.

view this post on Zulip Email Gateway (Aug 18 2022 at 14:41):

From: Michael Norrish <Michael.Norrish@nicta.com.au>
Actually, I see now that I can omit the term by using Named [] or
Positional [], which I guess is appropriate because I don't want to
pass any parameters to the one parent locale. But then, I still need to
provide two strings in the 'term expr, one of them coupled with a
boolean. The old code's globloc is a single string; and what of that boolean?

Michael

view this post on Zulip Email Gateway (Aug 18 2022 at 14:42):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Michael,

I admit the answer is not that easy to retrieve from the sources.

Actually, I see now that I can omit the term by using Named [] or
Positional [], which I guess is appropriate because I don't want to
pass any parameters to the one parent locale.

Exactly.

But then, I still need to
provide two strings in the 'term expr, one of them coupled with a
boolean. The old code's globloc is a single string; and what of that
boolean?

The first string is the name of the locale to import; the pair string * bool is the prefix to be added to the imports from the specified locale,
together with a flag indicating whether the prefix is mandatory.

Hope this helps,
Florian
signature.asc


Last updated: May 06 2024 at 16:21 UTC