[isabelle-dev] NEWS: document preparation refinements

[Makarius]

*** 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