equal
deleted
inserted
replaced
315 val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " " |
315 val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " " |
316 val parse_value = |
316 val parse_value = |
317 Scan.repeat1 (Parse.minus >> single |
317 Scan.repeat1 (Parse.minus >> single |
318 || Scan.repeat1 (Scan.unless Parse.minus |
318 || Scan.repeat1 (Scan.unless Parse.minus |
319 (Parse.name || Parse.float_number)) |
319 (Parse.name || Parse.float_number)) |
320 || Parse.$$$ "," |-- Parse.number >> prefix "," >> single) |
320 || @{keyword ","} |-- Parse.number >> prefix "," >> single) |
321 >> flat |
321 >> flat |
322 val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) [] |
322 val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) [] |
323 val parse_params = |
323 val parse_params = |
324 Scan.optional (Parse.$$$ "[" |-- Parse.list parse_param --| Parse.$$$ "]") [] |
324 Scan.optional (@{keyword "["} |-- Parse.list parse_param --| @{keyword "]"}) [] |
325 |
325 |
326 fun handle_exceptions ctxt f x = |
326 fun handle_exceptions ctxt f x = |
327 f x |
327 f x |
328 handle ARG (loc, details) => |
328 handle ARG (loc, details) => |
329 error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details ^ ".") |
329 error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details ^ ".") |