| 8472 | */ |
| 8473 | |
| 8474 | const delimTypeToFont = function delimTypeToFont(type) { |
| 8475 | if (type.type === "small") { |
| 8476 | return "Main-Regular"; |
| 8477 | } else if (type.type === "large") { |
| 8478 | return "Size" + type.size + "-Regular"; |
| 8479 | } else if (type.type === "stack") { |
| 8480 | return "Size4-Regular"; |
| 8481 | } else { |
| 8482 | throw new Error(`Add support for delim type '${type.type}' here.`); |
| 8483 | } |
| 8484 | }; |
| 8485 | /** |
| 8486 | * Traverse a sequence of types of delimiters to decide what kind of delimiter |
| 8487 | * should be used to create a delimiter of the given height+depth. |