/* Show the per-result buttons -- permalink, jump-to-proof, "Uses", Lean
   declarations -- at all times. The theme reveals them only while the pointer
   rests on the heading (theme-white.css: div.thm_header_hidden_extras is
   display:none, undone by div[class$=_thmheading]:hover), which leaves them
   unreachable on a touch screen. This file is the last stylesheet the pages
   load, so the rule wins. */
div.thm_header_hidden_extras {
	display: inline-block;
}

/* The checkmark that marks a formalised result carries no information where every
   result is formalised, so it stays out of the heading. */
div.thm_header_extras {
	display: none;
}

/* On a narrow window the heading of a result wraps, and the icon bar (permalink,
   proof, Uses, Lean) takes a line of its own under "Theorem 1.1 (Title)" instead of
   squeezing the title. */
@media (max-width: 640px) {
	div[class$=_thmheading] {
		flex-wrap: wrap;
	}

	div.thm_header_hidden_extras {
		flex-basis: 100%;
		margin-top: 0.15rem;
	}
}

/* Vertical-line markers for theorem statements and proofs. */

div.theorem_thmcontent {
	border-left: .15rem solid black;
}

div.proposition_thmcontent {
	border-left: .15rem solid black;
}

div.lemma_thmcontent {
	border-left: .1rem solid black;
}

div.corollary_thmcontent {
	border-left: .1rem solid black;
}

div.proof_content {
	border-left: .08rem solid grey;
}

/* Smaller dependency-graph legend, with tighter colon spacing and a little
   more separation between entries. */
#Legend dl.legend {
	line-height: 1.1;
}

#Legend dl.legend dt,
#Legend dl.legend dd {
	font-size: 0.72rem;
}

#Legend dl.legend dt {
	margin-top: 0.35rem;
}

/* Less space after the ":" (overrides dep_graph.css's .5rem). */
#Legend dl.legend dd {
	margin-left: 0.15rem;
}

#legend_title {
	font-size: 0.9rem;
}

/* Room to scroll past the end of both panes. They are the two overflow:auto
   containers, and the theme drops div.content's bottom margin from 1024px up,
   so the last line of a page and the last entry of the table of contents end up
   flush against the window edge and can be clipped. Padding on the scroll
   container extends the scrollable area; a margin on its last child would not. */
div.content {
	padding-bottom: 4rem;
}

nav.toc {
	padding-bottom: 4rem;
}

/* Room after every statement and more after every proof, so that what follows starts
   clearly apart. */
div[class*="_thmwrapper"] {
	margin-bottom: 1rem;
}

div.proof_wrapper {
	margin-bottom: 2.5rem;
}

/* The two link lines on the title page, added below the author by the workflow:
   close to the author and to each other, with room before the page goes on. */
div.titlepage p.authors {
	margin-bottom: 0.15rem;
}

div.titlepage p.repo-link {
	margin: 0.15rem 0;
}

div.titlepage p.repo-link:last-of-type {
	margin-bottom: 2rem;
}

/* The header of the dependency-graph page. dep_graph.css lays the title absolutely over
   the whole header, centred, while the Home link sits left in the flow, so a long title
   runs over the link on a narrow window. In the flow beside the link the two cannot
   overlap; the title takes the remaining width, is centred there, and wraps and shrinks
   on phones. The header may then grow beyond its fixed 3rem, and no header shrinks for
   the content below it, which clipped a title of several lines on a phone. */
body > header {
	flex-shrink: 0;
}

body > header h1#doc_title {
	position: static;
	flex: 1;
	margin: 0;
	padding: 0 .5rem;
	text-align: center;
	line-height: 1.2;
}

body > header a.toc {
	margin-right: 0;
}

body > header:has(> h1#doc_title) {
	height: auto;
	min-height: 3rem;
}

@media (max-width: 600px) {
	body > header h1#doc_title {
		font-size: 1.1rem;
	}
}

/* The statement that opens on a click in the dependency graph fits the window:
   dep_graph.css gives it a fixed width but no height limit, so a long statement
   ran below the window edge and could only be read after zooming out. Now it
   is at most as tall as the window below the header and scrolls inside. */
div.dep-modal-content {
	max-height: calc(100vh - 6rem);
	overflow: auto;
	box-sizing: border-box;
}