body {
	margin: 0px;
	scrollbar-width: none;
	-ms-overflow-style: none;
}

body::-webkit-scrollbar {
	display: none;
}

.hamburger-div, .hamburger-section-link {
	cursor: pointer;
}

.pattern-title {
	display: inline-block;
	font-family: sans-serif;
	font-weight: bold;
	text-align: left;
	padding-left: 1em;
	margin-right: 1em;
}

.production-desc {
	width: calc(100vw - 100px);
}

.pattern {
	display: inline-block;
	font-family: monospace;
	font-size: 16px;
}

.lexical-description {
	margin-top: 1em;
	padding-left: 2em;
}

.production-block {
	font-family: sans-serif;
	line-height: 1.35em;
	text-wrap: nowrap;
	overflow-x: scroll;
	scrollbar-width: none;
	-ms-overflow-style: none;
}

.production-or-block {
	font-family: sans-serif;
	line-height: 1.35em;
	text-wrap: nowrap;
	overflow-x: scroll;
	scrollbar-width: none;
	-ms-overflow-style: none;
}

.production-nested-block {
	font-family: sans-serif;
	line-height: 1.35em;
	scrollbar-width: none;
	-ms-overflow-style: none;
}

.production-block::-webkit-scrollbar, .production-or-block::-webkit-scrollbar, .production-nested-block::-webkit-scrollbar {
	display: none;
}

.production-needs-testing {
	background: red;
}

.production-number {
	display: inline-block;
	width:2em;
	text-align: right;
	margin-right: 0.5em;
}

.production-name {
	display: inline-block;
	min-width: 20em;
	text-align: right;
	font-weight: bold;
	margin-right: 0.5em;
}

.production-op {
	display: inline-block;
	width: 1.5em;
	font-weight: bold;
	margin-right: 0.5em;
}

.production-or {
	display: inline-block;
	font-weight: bold;
	text-align: right;
	width: 24em;
	margin-right: 1.5em;
}

.production-nested {
	display: inline-block;
	font-weight: bold;
	text-align: right;
	width: 26em;
	margin-right: 1.5em;
}

.production-reference {
	display: inline;
	font-style: italic;
}

.production-token {
	display: inline;
	font-weight: bold;
}

.production-many {
	display: inline;
    vertical-align: super;
    font-size: smaller;
    line-height: normal;
}

.section-description {
	display: block;
	margin-top: 1.5em;
	margin-left: 5em;
	max-width: 50em;	
}

p.comment {
	background-color: yellow;
}

.hidden {
	display: none;
}