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

On Mon, 1 Dec 2008, Josef Urban wrote:

> Comments in programming languages serve as a general storage for 
> anything that the language does not capture yet. If there is a frequent 
> need for expressing certain annotations, such annotations should be 
> eventually made more formal and taken care of by extending the 
> language's syntax. I think Isabelle/Isar has done this, and the result 
> is that it is much easier to write publishable papers about Isar 
> formalizations (or more precisely: the formalizations can already 
> contain all the TeX documentation/paper).

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