| 8597 | */ |
| 8598 | |
| 8599 | var delimTypeToFont = function delimTypeToFont(type) { |
| 8600 | if (type.type === "small") { |
| 8601 | return "Main-Regular"; |
| 8602 | } else if (type.type === "large") { |
| 8603 | return "Size" + type.size + "-Regular"; |
| 8604 | } else if (type.type === "stack") { |
| 8605 | return "Size4-Regular"; |
| 8606 | } else { |
| 8607 | throw new Error("Add support for delim type '" + type.type + "' here."); |
| 8608 | } |
| 8609 | }; |
| 8610 | /** |
| 8611 | * Traverse a sequence of types of delimiters to decide what kind of delimiter |
| 8612 | * should be used to create a delimiter of the given height+depth. |