doc-src/IsarRef/syntax.tex

 \subsection{Comments}\label{sec:comments}
 
 Large chunks of plain \railqtoken{text} are usually given
 \railtoken{verbatim}, i.e.\ enclosed in \verb|{*|~\dots~\verb|*}|.  For
 convenience, any of the smaller text units conforming to \railqtoken{nameref}
-are admitted as well.  Almost any of the Isar commands may be annotated by a
+are admitted as well.  Almost any of the Isar commands may be annotated by
 marginal \railnonterm{comment} of the form \texttt{--} \railqtoken{text}.
 Note that the latter kind of comment is actually part of the language, while
 source level comments \verb|(*|~\dots~\verb|*)| are stripped at the lexical
 level.  A few commands such as $\PROOFNAME$ admit additional markup with a
 ``level of interest'': \texttt{\%} followed by an optional number $n$ (default

 
 \indexoutertoken{text}\indexouternonterm{comment}\indexouternonterm{interest}
 \begin{rail}
   text: verbatim | nameref
   ;
-  comment: '--' text
+  comment: ('--' text +)
   ;
   interest: percent nat? | ppercent
   ;
 \end{rail}