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

On Sun, 14 Dec 2008, trybulec wrote:

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

Independently from the Mizar parser? I think complete independence (i.e., 
putting metadata into comments) is suboptimal (though certainly better to 
have metadata in comments than not at all). For presenting in HTML (and 
other systems), it would be good if metadata were present in the XML form 
of article produced by the Mizar parser. That means the parser should be 
aware of them, at least to some minimal extent (e.g., recognize the start 
and end bracket of metadata, and treat everything in between as a string, 
and output this in a proper place in the XML).

> I hope we will reach common solution with other systems.

One standard is the Dublin Core (DC), my Perl hack currently produces 
proper DC XML elements from the starting comments in .miz files. There is 
no reason why the Mizar parser could not do it too from whatever 
human-friendly syntax.

Josef