Re: [isabelle] updating code that calls add_locale_i



On 11/02/10 11:39, Michael Norrish wrote:

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.

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.