(value: string | undefined)
| 35 | } |
| 36 | |
| 37 | function jsonLiteral(value: string | undefined): string { |
| 38 | if (value === undefined) return 'undefined' |
| 39 | return JSON.stringify(value).replace(/</g, '\\u003c').replace(/>/g, '\\u003e') |
| 40 | } |
| 41 | |
| 42 | function htmlClose( |
| 43 | message: string, |