1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
@namespace url(http://www.w3.org/1999/xhtml);
@namespace svg url(http://www.w3.org/2000/svg);
body {
/* Trim down the default top margin of 8px, so we have a bit more space. */
margin-top: 4px;
}
div.threadnamediv {
height: 16px;
}
div.threadnamesdiv {
margin-right: 2px;
position: absolute;
font-family: monospace;
z-index: -1;
}
/* The fakescrolldiv will have the scroll bar, the amount it scrolls is
controlled by the size of fattydiv within it. */
div.fakescrolldiv {
/* This needs to be at least 16px, the height of the scrollbar, to have the
scrollbar renderer in firefox */
/* Making the height 16px in webkit causes the computed width to be 16px
shorter than what we specify. 17px is enough to cause it to be correct */
height: 17px;
width: 1008px;
overflow: auto;
}
div.fattydiv {
/* the div needs to have a height for the scrollbar to render in firefox */
height: 1px;
}
div.infoareadiv {
margin-top: 4px;
padding: 4px;
border: 1px solid gray;
height: 350px;
overflow: auto;
font-family: monospace;
white-space: pre;
}
svg|rect.thread {
/* fill: #f4f4f6; */
fill: #efeff2;
opacity: 0.7;
}
svg|rect.event {
fill: #f6a120;
}
svg|rect.eventwaiting {
fill: #62ccf3;
}
svg|rect.event:hover, svg|rect.eventwaiting:hover {
fill: #d92129;
}
svg|line.eventline {
stroke: #bad432;
stroke-width: 2px;
stroke-opacity: 0.7;
}
svg|line.eventline:hover {
stroke: #d92129;
stroke-opacity: 1;
}
|
