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

Josef Urban wrote:

>
> The difference is in reconstructing the article in HTML. The syntax in 
> comments allows users to do stupid things like:
>
> theorem Foo
> a+b =
> ::?SECTION Blah
> b+a
> proof ... end;
>
> It is easy for the Mizar parser to disallow this stupidity. It is not 
> easy for a lightweight parser which is not aware of the standard Mizar 
> syntax.


A good argument. The place of this pragma must be controlled. Perhaps 
some others, too.  Does it mean
that we should introduce a reserved word for it?

section XXXX;

It results in an advantage for the parser: better reporting of errors. 
E.g. reporting unpaired 'proof'.

Merry Christmass,

Andrzej