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

Hi:

Thanks for the explanation.

It would be nice to same same mark commands in Coq and Mizar, and other 
systems, too.

The reason of designing XML was to have a uniform solution to it. I 
still do not understand why

<AUTHOR>
   XXX YYY
</AUTHOR>

is so much less readable than

 author XXX YYY;

or

 author {* XXX YYY *}

Regards,
Andrzej Trybulec

Makarius wrote:

>Isabelle/Isar supports basically three kinds of "comments":
>
>  (1) Source comments  (* like this *)  which are stripped from the text
>      as it is being processed, i.e. they behave like comments in most 
>      programming languages, or % in TeX.
>
>  (2) Document comments  -- {* like this *}  which are considered part of 
>      the formal langaguage and are included in the final typesetting.
>
>  (3) Explicit markup commands, notably
>
>      chapter {* ... *}
>      section {* ... *}
>      subsection {* ... *}
>      text {* ... *}
>
>      These are full commands, just like 'theorem' or 'proof', but the do 
>      not affect the logical context.
>
>The argument text {* ... *} of document comments and markup commands can 
>refer to logical entities from the context of the text, by using document 
>antiquotations.  For example:
>
>  text {* blah blah @{term "x + y = z"} blah blah @{thm lemma1} ... *}
>
>These antiquotations are checked according to the full logical context, 
>and pretty printed with the syntax of the context (although I would prefer 
>annotating the original input source, instead of printing internal 
>entities).
>
>
>Since this thread was initially about meta data for theories, what we have 
>in Isabelle/Isar is only this:
>
>	header {* ... *}
>
>	theory A ...
>	begin
>	   ...
>	end
>
>Here the 'header' provides free-form text, it is usually typeset like 
>'section'.  Adding extra commands for 'author' etc. would be straight 
>forward, but we have never really needed this yet.  In Isabelle/Isar 
>documents the title/author is usually part of the outermost root.tex that 
>assembles all the generated LaTeX sources in the end.
>
>
>	Makarius
>
>  
>