# HG changeset patch
# User wenzelm
# Date 945890959 -3600
# Node ID 5c7b133fd26ff16bd25b408072f6564f49b53cc4
# Parent  ef78716f39ef67e7030a05034be261c0b24895ba
marg_comment: repeat;

diff -r ef78716f39ef -r 5c7b133fd26f src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Wed Dec 22 20:28:56 1999 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Wed Dec 22 20:29:19 1999 +0100
@@ -161,8 +161,8 @@
 
 (* 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;