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