Re: an extension of the mizar language for dealing with article metadata

Josef Urban wrote:

>
>
> But I think syntax like:
>
> <Theorem kind="T"> <For> <Typ kind="G" nr="15"> <Cluster> <Adjective 
> nr="204"/> <Adjective nr="259"/> <Adjective nr="261"/> </Cluster> 
> </Typ> <For> ...
>
> would not be particularly attractive as a language for human 
> mathematicians.
>

I completely agree. I propose XML only for metadata. I am even not sure 
if "propose" is a correct word.
I would not reject such solution.

> I agree that if there is just little markup like in your example, it 
> is not a big deal. XML is really a good technology, but using it 
> extensively for humans is a misuse in my opinion. One good reason for 
> having things like XML, Lisp and Prolog, is that they are easy to 
> parse. But it is strange to use this reason in our situation, because 
> Mizar already has a very complex parser (producing XML from the 
> natural syntax) anyway.


Right. But I believe that the metadata probably will evolve 
independently and I hope we will reach common solution with other 
systems. So I would like to have them separated from "pure" Mizar.

Regards,
Andrzej