equal
deleted
inserted
replaced
45 val bracks: (T list -> 'a * T list) -> T list -> 'a * T list |
45 val bracks: (T list -> 'a * T list) -> T list -> 'a * T list |
46 val mode: string -> 'a * T list -> bool * ('a * T list) |
46 val mode: string -> 'a * T list -> bool * ('a * T list) |
47 val maybe: (T list -> 'a * T list) -> T list -> 'a option * T list |
47 val maybe: (T list -> 'a * T list) -> T list -> 'a option * T list |
48 val name: T list -> string * T list |
48 val name: T list -> string * T list |
49 val symbol: T list -> string * T list |
49 val symbol: T list -> string * T list |
|
50 val liberal_name: T list -> string * T list |
50 val nat: T list -> int * T list |
51 val nat: T list -> int * T list |
51 val int: T list -> int * T list |
52 val int: T list -> int * T list |
52 val var: T list -> indexname * T list |
53 val var: T list -> indexname * T list |
53 val list: (T list -> 'a * T list) -> T list -> 'a list * T list |
54 val list: (T list -> 'a * T list) -> T list -> 'a list * T list |
54 val list1: (T list -> 'a * T list) -> T list -> 'a list * T list |
55 val list1: (T list -> 'a * T list) -> T list -> 'a list * T list |
249 fun mode s = Scan.lift (Scan.optional (parens ($$$ s) >> K true) false); |
250 fun mode s = Scan.lift (Scan.optional (parens ($$$ s) >> K true) false); |
250 fun maybe scan = $$$ "_" >> K NONE || scan >> SOME; |
251 fun maybe scan = $$$ "_" >> K NONE || scan >> SOME; |
251 |
252 |
252 val name = named >> sym_of; |
253 val name = named >> sym_of; |
253 val symbol = symbolic >> sym_of; |
254 val symbol = symbolic >> sym_of; |
|
255 val liberal_name = symbol || name; |
254 |
256 |
255 val nat = some_ident Syntax.read_nat; |
257 val nat = some_ident Syntax.read_nat; |
256 val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *; |
258 val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *; |
257 val var = some_ident Syntax.read_variable; |
259 val var = some_ident Syntax.read_variable; |
258 |
260 |