[isabelle-dev] Remaining uses of {* ... *} quotation?

[Makarius]

On 08/11/2018 21:36, Lawrence Paulson wrote:
>> On 8 Nov 2018, at 20:32, Makarius <makarius at sketis.net> wrote:
>>
>> In particular, what are the remaining uses of {* ... *}?
> 
> I didn’t even know that existed.

It was used a lot with the 'section' and 'text' commands until recently.
That was actually its main motivation approx. 20 years ago: to delimit
LaTeX sources reliably.

Now the occurrence of {* ... *} in some existing sources makes them look
very old-fashioned, but "isabelle update_cartouches -t" does a thorough
job automatically.


> But I use (*...*) to enclose arbitrary text or comment material out.

Outer comment syntax will remain unchanged: its main purpose is to
comment-out material temporarily, or to write meta-comments (like % in
LaTeX).

Proper document text would normally appear within cartouches and marked
by 'text' or \<comment>.


	Makarius