(s, style)
| 395 | · value: option value`; |
| 396 | |
| 397 | function splitPrintOptions(s, style) { |
| 398 | const m = /^\/(\w+)/.exec(s); |
| 399 | if (!m) |
| 400 | return [s, style]; |
| 401 | if (m[1].startsWith('p')) |
| 402 | style.pretty = true; |
| 403 | if (m[1].startsWith('b')) |
| 404 | style.brief = true; |
| 405 | return [s.substr(m[0].length).trimStart(), style]; |
| 406 | } |
| 407 | |
| 408 | function doPrint(expr, style) { |
| 409 | // This is the real deal. |