Re: [isabelle-dev] NEWS: document preparation refinements

2015-10-26 Thread Makarius
On Mon, 26 Oct 2015, Tobias Nipkow wrote: On 23/10/2015 23:16, Makarius wrote: * The @{text} antiquotation now ignores the antiquotation option "source". The given text content is output unconditionally, without any surrounding quotes etc. Subtle INCOMPATIBILITY, put quotes into the

Re: [isabelle-dev] NEWS: document preparation refinements

2015-10-26 Thread Tobias Nipkow
Thanks, that did the trick. Tobias On 26/10/2015 18:16, Makarius wrote: On Sat, 24 Oct 2015, Tobias Nipkow wrote: 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

Re: [isabelle-dev] NEWS: document preparation refinements

2015-10-26 Thread Makarius
On Sat, 24 Oct 2015, Tobias Nipkow wrote: 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

Re: [isabelle-dev] NEWS: document preparation refinements

2015-10-23 Thread Makarius
Some more NEWS items (Isabelle/436b7fe89cdc): *** Document preparation *** * There is a new short form for antiquotations with a single argument that is a cartouche: \<^name>‹...› is equivalent to @{name ‹...›} and ‹...› without control symbol is equivalent to @{cartouche ‹...›}. The standard

[isabelle-dev] NEWS: document preparation refinements

2015-10-19 Thread 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