On Fri, 28 Nov 2008, trybulec wrote:
> Josef Urban wrote:
>
>>
>> This is written in Jesse's e-mail: the metadata could be processed by
>> standard Mizar-based tools that are currently used for creating the HTML
>> representation, are (going to be) used for collecting data for MML
>> Query, and possibly also other things like FM and MPTP. It is not
>> practical to keep these data separately and process them by separate
>> tools, especially when they are quite a natural part of the articles.
>>
> 'natural' ?
>
> Well, if you mean by an 'article' a mathematical paper you're right, if it
> is thought as a script for the verifier, you're not.
So why is the keyword "begin" allowed multiple times to introduce
sections, and why do all articles start with the standard header
containing author and title, why are comments allowed at all? If there
is no need to process and present these article parts in HTML, MML Query,
FM, MPTP, etc., I suggest to disallow these "unnatural" parts also in the
article (.miz) files. Or perhaps they are useful, and we should properly
care about them? Writing fragile Perl hacks that will hardly be usable on
Windoze is then hardly the right way: the Mizar parser should do this.
Josef
>
> Regards,
> Andrzej
>
