[isabelle-dev] NEWS: document preparation refinements

[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
>>  argument where they are really intended, e.g. @{text ‹"foo"›}. Initial
>>  or terminal spaces are ignored.
>
> I have wanted the surrounding quotes that come with [source] to go away since 
> day 1. Unfortunately the above change does not solve my `problem': I have 
> many occurrences of @{term[source]} where I have to remove " explicitly by 
> wrapping my own \noquotes macro around it.

I know.

The reason why @{text} no longer prints the source quotes is that it is no 
longer a member of the class of "standard" antiquotations @{typ},
@{term}, {prop}, @{thm}.  Instead it does its own well-defined business.

The standard antiquotations like @{term} did not change so far, and 
require more thoughts in the future. Inlining formal material into the 
generated document needs to be done differently, such that it fits with 
the PIDE document model of semantic markup.


Morover, the use of double quote notation itself is gradually on retreat: 
more and more cartouches show up in syntax definitions.

Cartouches have many advantages.  E.g. there is a clear concept to add or 
remove a level of cartouche quotation, without having to worry about 
escaped quotes in the body.

A disadvantage is that cartouches everywhere (with lots of nesting) look 
more boring than varying quotes, a bit like LISP.  Or is that modesty in 
syntax an advantage as well?


 	Makarius