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

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

Josef Urban wrote:

> XML is easy to process by machines, and it is for this reason used as 
> the Mizar internal layer and input for other systems. Mizar parser 
> produces the XML from the Mizar human-like text, and I think it should 
> stay this way. That is: human-like keywords for humans, processed into 
> machine-understandable XML by Mizar parser.
>
> The metadata info should certainly be optional during verification and 
> only required (if at all) when the article is submitted. I don't think 
> that broadening this discussion to other "pragmas" is going to help to 
> fix the problem Jesse asked about in a reasonable time. Inability to 
> present the metadata in HTML is a bug that should be fixed quickly, 
> discussing new Mizar features is useful but should be done separately 
> and not in this context .


As I wrote I have no opinion on the topic. I hoped that you would 
support XML :-)

On the other hand why not put the metadata into an unremovable comment, 
starting e.g. with
::$

More serious problem: what do you mean by 'Inability to present the 
metadata in HTML' ?

Regards.
Andrzej