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 also 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.
Scribble used to support a custom style for optional brackets. In particular, the optional brackets will be given the
'paren-shapeof value#\?[1], and the CSS classopt-colorwill be tagged to these brackets.Later, Scribble supports the curry notation. Its implementation no longer uses
'paren-shapeto indicate optional brackets. Unfortunately, it also accidentally dropped theopt-colortagging[2].This PR restores the original behavior by tagging the class
opt-colorto optional brackets. It also addsracketoptionalfontso that Scribble users can typeset optional brackets. Lastly, it cleans up the code that supports the'paren-shapeof 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.