Re: vocabularies

On Tue, 6 Jan 2009, Grzegorz Bancerek wrote:

>> The FM translation technology should rather use notation (pattern) for 
>> mapping to TeX than the symbol level, because one Mizar symbol can have 
>> very different contexts of use, and possibly very different TeX notations 
>> (I think we already talked about this one with Grzegorz some time ago).
>
> In FM translation the only almost but not quite unlike stable resource is 
> used:
> formats (symbol+arity). For example, plus in expressions x+y, x+, +x etc.
> may have different presentation in LaTeX. Namely, the first and third pluses 
> are
> represented just by + but the second by ^+
> Of course, there are bigger differences in translation for other symbols.
>
> Patterns uses types of arguments annotated with constructors which change 
> from
> version to version of distribution. Maintenance of translation patterns based 
> on
> such resource may be quite interesting.

I think there is one simple option: keep the TeX symbol in the article 
with the definition if needed. There could still be the current table on 
the format level used as a default (e.g. x+y will most often be x+y in 
TeX), and the info from patterns would override the format default (if 
there is any).

My knowledge of the current FM translation technology is limited, but I 
think this could take care of the maintenance problem and also allow the 
users to easily provide new TeX presentation info directly in the article 
(without learning about FM formats).

Josef