equal
deleted
inserted
replaced
179 fun args blk x = Scan.optional (args1 blk) [] x |
179 fun args blk x = Scan.optional (args1 blk) [] x |
180 and args1 blk x = |
180 and args1 blk x = |
181 ((Scan.repeat1 |
181 ((Scan.repeat1 |
182 (Scan.repeat1 (atom_arg blk) || |
182 (Scan.repeat1 (atom_arg blk) || |
183 paren_args "(" ")" args || |
183 paren_args "(" ")" args || |
184 paren_args "{" "}" args || |
|
185 paren_args "[" "]" args)) >> flat) x; |
184 paren_args "[" "]" args)) >> flat) x; |
186 |
185 |
187 |
186 |
188 |
187 |
189 (** type src **) |
188 (** type src **) |