equal
deleted
inserted
replaced
226 |
226 |
227 |
227 |
228 (* names and text *) |
228 (* names and text *) |
229 |
229 |
230 val name = group "name declaration" (short_ident || sym_ident || string || number); |
230 val name = group "name declaration" (short_ident || sym_ident || string || number); |
231 val binding = position name >> Name.binding_pos; |
231 val binding = position name >> Binding.binding_pos; |
232 val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number); |
232 val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number); |
233 val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim); |
233 val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim); |
234 val path = group "file name/path specification" name >> Path.explode; |
234 val path = group "file name/path specification" name >> Path.explode; |
235 |
235 |
236 val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") ""; |
236 val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") ""; |