src/Pure/Isar/outer_parse.ML

 val text = group "text" (short_ident || long_ident || sym_ident || string || verbatim);
 
 
 (* formal comments *)
 
-val comment = text >> Comment.plain;
-val marg_comment = Scan.optional ($$$ "--" |-- comment) Comment.none;
+val comment = text >> (Comment.plain o Library.single);
+val marg_comment = Scan.repeat ($$$ "--" |-- text) >> Comment.plain;
 
 val interest = Scan.optional ($$$ "%%" >> K Comment.no_interest ||
   $$$ "%" |-- Scan.optional nat 1 >> Comment.interest) Comment.default_interest;