| changeset 58864 | 505a8150368a |
| parent 57905 | c0c5652e796e |
| child 58923 | cb9b69cca999 |
| 58863:64e571275b36 | 58864:505a8150368a |
|---|---|
103 |
103 |
104 in |
104 in |
105 |
105 |
106 val parse_elements = |
106 val parse_elements = |
107 Source.of_list #> |
107 Source.of_list #> |
108 Source.source stopper (Scan.bulk other_element) NONE #> |
108 Source.source stopper (Scan.bulk other_element) #> |
109 Source.exhaust; |
109 Source.exhaust; |
110 |
110 |
111 end; |
111 end; |
112 |
112 |
113 end; |
113 end; |