*** 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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
