diff -r 15261d78d7b5 -r eebb8270b3cc src/Doc/Sugar/Sugar.thy --- a/src/Doc/Sugar/Sugar.thy Fri Feb 07 21:27:11 2025 +0100 +++ b/src/Doc/Sugar/Sugar.thy Sat Feb 08 11:18:30 2025 +0100 @@ -533,9 +533,9 @@ You have to place the following lines before and after the snippet, where snippets must always be consecutive lines of theory text: \begin{quote} -\verb!\text_raw{!\verb!*\snip{!\emph{snippetname}\verb!}{1}{2}{%*!\verb!}!\\ +\verb!\text_raw\!\verb!\snip{!\emph{snippetname}\verb!}{1}{2}{%\!\verb!!\\ \emph{theory text}\\ -\verb!\text_raw{!\verb!*!\verb!}%endsnip*!\verb!}! +\verb!\text_raw\!\verb!%endsnip\!\verb!! \end{quote} where \emph{snippetname} should be a unique name for the snippet. The numbers \texttt{1} and \texttt{2} are explained in a moment.