# HG changeset patch
# User wenzelm
# Date 947069898 -3600
# Node ID 424f6e663977a46ebc1978d7539937fa47b4a184
# Parent  ae555dd9585b9d6889e0e1e7f9a5fea02d723041
comment: any number of texts;

diff -r ae555dd9585b -r 424f6e663977 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Wed Jan 05 11:57:47 2000 +0100
+++ b/doc-src/IsarRef/syntax.tex	Wed Jan 05 11:58:18 2000 +0100
@@ -115,7 +115,7 @@
 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
@@ -129,7 +129,7 @@
 \begin{rail}
   text: verbatim | nameref
   ;
-  comment: '--' text
+  comment: ('--' text +)
   ;
   interest: percent nat? | ppercent
   ;