equal
deleted
inserted
replaced
258 |
258 |
259 (** outer syntax **) |
259 (** outer syntax **) |
260 |
260 |
261 local structure P = OuterParse and K = OuterKeyword in |
261 local structure P = OuterParse and K = OuterKeyword in |
262 |
262 |
263 val _ = OuterSyntax.keywords ["morphisms"]; |
263 val _ = OuterKeyword.keyword "morphisms"; |
264 |
264 |
265 val typedef_decl = |
265 val typedef_decl = |
266 Scan.optional (P.$$$ "(" |-- |
266 Scan.optional (P.$$$ "(" |-- |
267 ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s))) |
267 ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s))) |
268 --| P.$$$ ")") (true, NONE) -- |
268 --| P.$$$ ")") (true, NONE) -- |