equal
deleted
inserted
replaced
254 |
254 |
255 |
255 |
256 (* outer syntax *) |
256 (* outer syntax *) |
257 |
257 |
258 local |
258 local |
259 val option_parser = Parse.group "option" |
259 val option_parser = Parse.group (fn () => "option") |
260 ((Parse.reserved "sequential" >> K Sequential) |
260 ((Parse.reserved "sequential" >> K Sequential) |
261 || ((Parse.reserved "default" |-- Parse.term) >> Default) |
261 || ((Parse.reserved "default" |-- Parse.term) >> Default) |
262 || (Parse.reserved "domintros" >> K DomIntros) |
262 || (Parse.reserved "domintros" >> K DomIntros) |
263 || (Parse.reserved "no_partials" >> K No_Partials) |
263 || (Parse.reserved "no_partials" >> K No_Partials) |
264 || ((Parse.reserved "invariant" |-- Parse.term) >> Invariant)) |
264 || ((Parse.reserved "invariant" |-- Parse.term) >> Invariant)) |