Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

make headSize and tailSize back into ArrowOpts fields #177

Merged
merged 1 commit into from
Apr 13, 2014

Commits on Apr 12, 2014

  1. make headSize and tailSize back into ArrowOpts fields

    As attributes, there are situations where it is actually impossible (or
    at least very difficult) to get things the way you want.  E.g. imagine
    creating a whole bunch of arrows via connectOutside and applyAll, but
    you want them to have all different head sizes.  I am not sure how to
    accomplish this via attributes at the moment.
    
    It is also simply annoying to have some arrow attributes set via
    ArrowOpts and some as normal attributes.  I ran into this when updating
    the website gallery, it was a confusing error and would have been
    annoying to fix.
    
    In the long term, I would love to have all arrow attributes be normal
    attributes... but that may have to wait until we have constraint solving
    and can declare arrows as separate standalone diagrams (to which
    attributes can be applied).
    
    Note this does mean deleting headSizeG, headSizeO, etc. It would be
    ideal to be able to write e.g. `... & headSizeG .~ 3 & ...`
    rather than `... & headSize (Global 3) & ...`, however, such a
    `headSizeG` would not be a valid lens.
    byorgey committed Apr 12, 2014
    Configuration menu
    Copy the full SHA
    303827f View commit details
    Browse the repository at this point in the history