/* This file contains CSS tweaks for this blueprint.
 * As an example, we included CSS rules that put
 * a vertical line on the left of 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;
}


/* --- Focused-subgraph controls on the dependency graph page ---------------
 * Added by `dep_graph_focus.js`, which restricts the graph to one node's
 * transitive dependencies. Loaded after dep_graph.css, so the #graph height
 * override below wins and the toolbar does not push the graph off-screen. */

div#focus-controls {
	display: flex;
	flex-wrap: wrap;
	align-items: center;
	gap: .4rem .6rem;
	padding: .4rem 0 .5rem 0;
	font-size: 95%;
}

div#focus-controls label {
	color: #444;
}

div#focus-controls input#focus-node {
	min-width: 22rem;
	flex: 1 1 22rem;
	padding: .2rem .4rem;
	border: 1px solid #497da5;
	border-radius: 4px;
	font: inherit;
}

div#focus-controls select {
	padding: .2rem;
	border: 1px solid #497da5;
	border-radius: 4px;
	font: inherit;
	background: white;
}

div#focus-controls button#focus-clear {
	padding: .2rem .6rem;
	border: 1px solid #497da5;
	border-radius: 4px;
	background: white;
	font: inherit;
	cursor: pointer;
}

div#focus-controls button#focus-clear:hover {
	background: #eef4f9;
}

div#focus-controls span#focus-status {
	margin-left: auto;
	color: #555;
	font-style: italic;
}

div#graph {
	height: calc(90vh - 3rem);
}

button.focus-link {
	margin-left: 1rem;
	padding: .1rem .5rem;
	border: 1px solid #497da5;
	border-radius: 4px;
	background: white;
	font-size: 90%;
	font-style: italic;
	cursor: pointer;
}

button.focus-link:hover {
	background: #eef4f9;
}

/* --- Suppress the per-node "Lean" links ----------------------------------
 * leanblueprint points these at `\dochome`/find/#doc/<decl>, i.e. at
 * https://stavan-jain.github.io/QECLean/docs — and nothing publishes anything
 * there, so every one of them falls through to 404.html and bounces the reader
 * to the qec-lab dashboard. A link that silently sends you somewhere unrelated
 * is worse than no link, so hide them until the docs exist.
 *
 * Dropping `\dochome` from web.tex would not help: leanblueprint then falls
 * back to mathlib's doc site, where none of these declarations exist either.
 *
 * `a.lean_decl` is the one class both renderings share -- chapter pages emit
 * `<a href="..." class="lean_decl">` inside the hover extras, the dependency
 * graph's modals emit `<a class="lean_link lean_decl">Lean</a>`.
 *
 * On a chapter page those anchors are the entire body of the `L∃∀N` button's
 * "Lean declarations" dialog, so hiding only the anchors would leave a button
 * that opens an empty box. Hide the button and its dialog as well. The dialog
 * is matched as the button's next sibling because it carries no class of its
 * own, and the sibling `uses` dialog must keep working.
 *
 * To restore: publish doc-gen4 output at `/docs` (see blueprint/README.md
 * § "The \lean{} links do not resolve yet") and delete this block. Nothing
 * else needs to change -- the links are generated, and are correct apart from
 * pointing at a directory that is not there. */

a.lean_decl,
button.modal.lean,
button.modal.lean + div.modal-container {
	display: none;
}