| java.lang.Object de.uka.ilkd.key.ocl.gf.MarkedAreaHighlightingStatus
MarkedAreaHighlightingStatus | class MarkedAreaHighlightingStatus (Code) | | Stores a MarkedArea together with some status fields, which tell
how it should get highlighted.
No direct highlighting stuff in here, that's done in GFEditor2
author: daniels |
focused | final boolean focused(Code) | | whether this MarkedArea is a subnode of the currently focused node
|
incorrect | final boolean incorrect(Code) | | whether this MarkedArea has (inherited) a GF constraint
|
ma | final MarkedArea ma(Code) | | The MarkedArea, which contains the highlighting information
|
MarkedAreaHighlightingStatus | public MarkedAreaHighlightingStatus(boolean focused, boolean incorrect, MarkedArea ma)(Code) | | Initializes this immutable record class
Parameters: focused - whether this MarkedArea is a subnode of the currently focused node Parameters: incorrect - whether this MarkedArea has (inherited) a GF constraint Parameters: ma - The MarkedArea, which contains the highlighting information |
|
|