/* The option-index filter table (docs/gen_options.py builds the rows). */
.opt-filter {
  width: 100%;
  padding: .6rem .8rem;
  font-size: .95rem;
  border: 1px solid var(--md-default-fg-color--lighter);
  border-radius: .25rem;
  background: var(--md-default-bg-color);
  color: var(--md-default-fg-color);
}
.opt-count { margin: .5rem 0 1rem; font-size: .75rem; color: var(--md-default-fg-color--light); }
.opt-row {
  padding: .5rem 0;
  border-bottom: 1px solid var(--md-default-fg-color--lightest);
}
.opt-row a { font-size: .9rem; }
.opt-row code { font-size: .85rem; }
.opt-row p {
  margin: .15rem 0 0;
  font-size: .8rem;
  color: var(--md-default-fg-color--light);
}
.opt-type {
  margin-left: .5rem;
  font-size: .7rem;
  padding: .1rem .4rem;
  border-radius: .2rem;
  background: var(--md-default-fg-color--lightest);
  color: var(--md-default-fg-color--light);
}
.opt-row[hidden] { display: none; }