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


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to