Switch to unified view

a b/docs/stylesheets/extra.css
1
small.subtitle {
2
  display: block;
3
  margin-top: -1.2em;
4
}
5
6
.definition-list-wrapper {
7
  font-size: .64rem;
8
  border: .05rem solid var(--md-typeset-table-color);
9
  border-radius: .1rem;
10
  border-bottom: none;
11
  margin-top: 1em;
12
}
13
14
.definition-list-wrapper > .title {
15
  border-bottom: .05rem solid var(--md-typeset-table-color);
16
  padding: 0.386029412em 1.1764705882em;
17
  background-color: #f5f5f5;
18
  font-weight: bold;
19
}
20
21
.definition-list-wrapper dl {
22
  margin-top: 0;
23
}
24
25
.definition-list-wrapper dl > div  {
26
  border-bottom: .05rem solid var(--md-typeset-table-color);
27
  padding: .7720588235em 1.1764705882em;
28
}
29
30
.definition-list-wrapper dl dt code {
31
  float: right;
32
  padding-left: 1em;
33
  padding-right: 1em;
34
}
35
36
.definition-list-wrapper dl dd {
37
  margin-top: 0;
38
  margin-bottom: 0;
39
}
40
41
.definition-list-wrapper dl dd p, .definition-list-wrapper dl ul {
42
  margin-top: 0.25em;
43
  margin-bottom: 0.5em;
44
}
45
46
.definition-list-wrapper details {
47
  background-color: transparent;
48
  border-color: var(--md-typeset-table-color);
49
}
50
51
.definition-list-wrapper summary {
52
  background-color: transparent;
53
  padding-top: 0.3rem;
54
  padding-bottom: 0.3rem;
55
  padding-left: 0.6rem !important;
56
}
57
58
.definition-list-wrapper summary:before {
59
  mask-image: none;
60
  -webkit-mask-image: none;
61
  background-color: transparent;
62
  width: 0;
63
}
64
65
.definition-list-wrapper summary:after {
66
  top: 0.325rem;
67
}
68
69
p.dimension-indicator {
70
  float: right;
71
  margin-top: 2em;
72
}
73
74
p.dimension-indicator code {
75
  padding-left: 1em;
76
  padding-right: 1em;
77
}
78
79
.attr-heading {
80
  margin-top: 1em;
81
  margin-bottom: -0.5em;
82
}
83
84
h4.attr-heading {
85
  font-weight: normal;
86
  letter-spacing: normal;
87
  margin-top: 2em;
88
  margin-bottom: -0.5em;
89
}
90
91
.indent {
92
  margin-left: 1.5em;
93
  margin-bottom: 1em;
94
}
95
96
.indent p {
97
  margin-top: 0.4em;
98
  margin-bottom: 0.4em;
99
}