[isabelle-dev] NEWS: uniform document heading commands

[Makarius]

On Mon, 3 Nov 2014, Timothy Bourke wrote:

> * Makarius <makarius at sketis.net> [2014-11-02 20:24 +0100]:
>> *** Document preparation ***
>>
>> * Document headings work uniformly via the commands 'chapter',
>> 'section', 'subsection', 'subsubsection' -- in any context, even
>> before the initial 'theory' command.
>
> Very nice. Thank you.
>
> Would it also be reasonable to allow 'text' before an initial 'theory' ?

Back to this additional point.  After reconsidering some other areas of 
document markup commands, I found that full uniformity comes as a natural 
consequence of some genuine simplifications, which are now in
Isabelle/ed09ae4ea2d8.

This means:

   * All document commands 'section', ..., 'text', 'text_raw' work in all
     situations: before the theory header, within the theory body, within
     proofs.  Note that antiquotations do require a proper context as
     before.

   * 'text' vs. 'txt' used to be specific theory vs. proof commands, but
     now they merely differ in the LaTeX style: \isastyletext vs.
     \isastyletxt.  It also means there is no longer a need to change LaTeX
     macros, if different styles are preferred.  Just use the command for
     the markup that you have in mind (e.g. see Isabelle/1c54ebc68394).

   * Since 'txt' was tagged as "proof" command, but is no longer special to
     proofs, I have removed that default tag.  In order to work as
     expected, such document commands (and diagnostic commands like 'thm')
     now retain the tagging of the present situation.  This also simplifies
     the general behaviour: accidental diagnostic commands within a proof
     document are treated as part of a proof, which is e.g. relevant when
     proofs are suppressed in the document (e.g. the "outline" in AFP).

   * Former 'txt_raw' is obsolete and already removed; just one 'text_raw'
     is sufficient for all situations.


Isn't life free and easy without the baggage of the TTY / Proof General 
mode?


 	Makarius

----------------------------------------------------------------------------
                   http://stop-ttip.org  894,773 people so far
----------------------------------------------------------------------------