On Mon, 3 Nov 2014, Timothy Bourke wrote:
* Makarius <makar...@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
----------------------------------------------------------------------------
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
