record Role : Type The role(s) an object (typically an atom or bond) in the
drawing currently has (for instance, it is selected, or
the mouse hovers over it, or it is currently being drawn).
We encode this as a bit pattern to facilitate adding new roles and
having several roles set simultaneously.
`Role` is a semigroup (using bitwise "or", `(.|.)`, for append) and
a monoid, with 0 as the neutral element.
Totality: total
Visibility: public export
Constructor: R : Bits8 -> Role
Projection: .role : Role -> Bits8
Hints:
Cast CDAtom Role Cast (Adj k b CDAtom) Role Cast (Context k b CDAtom) Role Cast CDBond Role Eq Role ModRole Role Monoid Role Ord Role Semigroup Role Show Role
.role : Role -> Bits8- Totality: total
Visibility: public export role : Role -> Bits8- Totality: total
Visibility: public export Selected : Role- Totality: total
Visibility: public export Persistent : Role- Totality: total
Visibility: public export Origin : Role- Totality: total
Visibility: public export None : Role- Totality: total
Visibility: public export New : Role- Totality: total
Visibility: public export HoverNew : Role- Totality: total
Visibility: public export Hover : Role- Totality: total
Visibility: public export Highlight : Role- Totality: total
Visibility: public export interface ModRole : Type -> Type Interface for objects with a `Role` we can modify
Parameters: a
Methods:
modRole : (Role -> Role) -> a -> a
Implementations:
ModRole CDAtom ModRole Role ModRole CDBond
modRole : ModRole a => (Role -> Role) -> a -> a- Totality: total
Visibility: public export setIf : ModRole a => Role -> Bool -> a -> a Sets the given role at an object in the drawing
Totality: total
Visibility: exportset : ModRole a => Role -> a -> a Sets the given role at an object in the drawing
Totality: total
Visibility: exportunset : ModRole a => Role -> a -> a Sets the given role at an object in the drawing
Totality: total
Visibility: exportkeep : ModRole a => Role -> a -> a Keep only the given roles and unset all others
Totality: total
Visibility: exportclear : ModRole a => a -> a Completely remove all roles
Totality: total
Visibility: exportis : Cast a Role => Role -> a -> Bool Tests if the given role(s) is/are set at the given object
in the drawing
Totality: total
Visibility: exportdata SelectMode : Type Selection mode we are currently in.
`Ignore` means that we are currently not selecting this type of item.
`One` means "single-select" mode (SHIFT is not down)
`Many` means "multi-select" mode (SHIFT is down)
Totality: total
Visibility: public export
Constructors:
Ignore : SelectMode One : SelectMode Many : SelectMode
selectIfHovered : ModRole a => SelectMode -> a -> a Selects a hovered node or edge.
The boolean flag indicates, if we want to keep already selected
node or not (as indicated by the `Shift` key being down).
Totality: total
Visibility: export