cbeee2d388
Scribble used to support a custom style for optional brackets.
In particular, the optional brackets will be given the `'paren-shape`
of value `#\?`[1], and the CSS class `opt-color` will be tagged
to these brackets.
Later, Scribble supports the curry notation. Its implementation
no longer uses `'paren-shape` to indicate optional brackets.
Unfortunately, it accidentally dropped the `opt-color` tagging[2].
This PR restores the original behavior by tagging the class
`opt-color` to optional brackets. It also adds `racketoptionalfont`
so that Scribble users can typeset optional brackets.
Lastly, it cleans up the code that supports the `'paren-shape` of value
`#\?`, since it is effectively a deadcode.
Note that this PR does _not_ change any CSS styling, so there's no
visible change. It would make CSS styling customization easier, however.
[1]:
|
||
|---|---|---|
| .. | ||
| scribble | ||