[mizar] vocabullaries

[trybulec <trybulec@math.uwb.edu.pl>]

FreeK:

Are you really serious about it?

Freek Wiedijk wrote:

> Of course _I_ always want the vocabulary files to be part
> of the articles.  It is a pain that they have their own
> name space, and that you need two files instead of one.
>
>  
Suppose that we want to implement program that extracts from the article 
its vocabulary. Syntactically we know
where the new symbols should occur. Almost E.g.
 
func a+b ...

there are 4 possibilities

a constant: the symbol 'a+b'
a prefix symbol: 'a+'
a postfix symbol: '+b'
an infix symbol: '+'

Either we have to adopt rule that new symbol must be separated by 
spaces, the it will be easy to extract it, or
to use the first identification (identification of identifiers) to find 
out what is the symbol. A small AI program.
What you would choose?

Of course we should do regular parsing (and before the tokenization) 
only in the place where a new symbol
may occur we suspend it.

Regards,
Andrzej