equal
deleted
inserted
replaced
160 |
160 |
161 (* formal comments *) |
161 (* formal comments *) |
162 |
162 |
163 val comment = text >> Comment.plain; |
163 val comment = text >> Comment.plain; |
164 val marg_comment = Scan.optional ($$$ "--" |-- comment) Comment.none; |
164 val marg_comment = Scan.optional ($$$ "--" |-- comment) Comment.none; |
165 val interest = Scan.optional ($$$ "%" >> K Comment.no_interest) Comment.default_interest; |
165 |
|
166 val interest = Scan.optional ($$$ "%%" >> K Comment.no_interest || |
|
167 $$$ "%" |-- Scan.optional nat 1 >> Comment.interest) Comment.default_interest; |
166 |
168 |
167 |
169 |
168 (* sorts and arities *) |
170 (* sorts and arities *) |
169 |
171 |
170 val sort = |
172 val sort = |