public class ExternalSettingsManager.ExternalSettings
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
IvMLogFiltered |
filteredLog |
int |
height |
double |
timeScale |
GraphVizTokensLazyIterator |
tokens |
TraceColourMap |
trace2colour |
java.awt.geom.AffineTransform |
transform |
int |
width |
Constructor and Description |
---|
ExternalSettings() |
public int width
public int height
public IvMLogFiltered filteredLog
public TraceColourMap trace2colour
public GraphVizTokensLazyIterator tokens
public java.awt.geom.AffineTransform transform
public double timeScale