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

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

On Sun, 30 Nov 2008, trybulec wrote:

> 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 
> :-)

See above: using XML for direct human reading/writing is in my opinion 
quite often abuse of a good technology developed for machines.

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

That could be a first step, if we don't want to bother with enhancing the 
Mizar parser. But if there is important information in such comments 
(title, author, sections, nice names of theorems, important comments, 
etc.) that will be used for presentation/searching/etc in HTML, FM, MML 
Query, etc., a parser for these things is needed anyway, so why not 
re-use the Mizar parser? Also, these things should appear in the XML form 
of the Mizar article, which is currently produced by the Mizar parser.

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

Metadata like title, author, etc. are not present in the XML 
representation of an article produced by the Mizar parser (because 
formally they are just ignored comments).

Josef