[isabelle-dev] NEWS: document preparation refinements

[Tobias Nipkow]

I don't know if this is related, but it must have happened recently: The 
[display] option for antiquotations now (eg 436b7fe89cdc) generates latex that 
indents the text following the display, even if there is no newline in between. 
This is in contrast to latex conventions (eg \[ \]) and I would rather not have 
to insert lots of \nondent by hand.

Tobias

On 19/10/2015 17:28, Makarius wrote:
> *** General ***
>
> * There is a new short form for antiquotations with a single argument
> that is a cartouche: \<^name>‹...› is equivalent to @{name ‹...›}.
>
>
> *** Prover IDE -- Isabelle/Scala/jEdit ***
>
> * Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls
> emphasized text style; the effect is visible in document output, not in
> the editor.
>
> * Action "isabelle-reset" now uses keyboard shortcut C+e BACK_SPACE,
> instead of former C+e LEFT.
>
>
> *** Document preparation ***
>
> * HTML presentation uses the standard IsabelleText font and Unicode
> rendering of Isabelle symbols like Isabelle/Scala/jEdit.  The former
> print mode "HTML" looses its special meaning.
>
> * Commands 'paragraph' and 'subparagraph' provide additional section
> headings. Thus there are 6 levels of standard headings, as in HTML.
>
> * Text is structured in paragraphs and nested lists, using notation that
> is similar to Markdown. The control symbols for list items are as
> follows:
>
>    ▪  itemize
>    ▸  enumerate
>    ➧  description
>
> * Text may contain control symbols for markup and formatting as follows:
>
>    ⇤   \noindent
>    ┈   \smallskip
>    ┉   \medskip
>    ━   \bigskip
>
> * Command 'text_raw' has been clarified: input text is processed as in
> 'text' (with antiquotations and control symbols). The key difference is
> the lack of the surrounding isabelle markup environment in output.
>
> * Document antiquotations @{emph} and @{bold} output LaTeX source
> recursively, adding appropriate text style markup. These are typically
> used in the short form ∗‹...› and ❙‹...›.
>
>
>
> All this refers e.g. to Isabelle/dcc8e1d34b18. The general trend is to make the
> editor view, LaTeX output and HTML output converge eventually, although we are
> still far from that.
>
> Examples for the Markdown paragraph/list notation and other control symbols can
> be seen in src/Doc: Implementation, Isar_Ref, JEdit, System.
>
>
>      Makarius
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5132 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151024/7c71a014/attachment.bin>