Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
marg_comment: repeat;
authorwenzelm
Wed, 22 Dec 1999 20:29:19 +0100
changeset 8077 5c7b133fd26f
parent 8076 ef78716f39ef
child 8078 c6da7585f9d1
marg_comment: repeat;
src/Pure/Isar/outer_parse.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle