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