ecmarkup.css 14KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783
  1. body {
  2. display: flex;
  3. font-size: 18px;
  4. line-height: 1.5;
  5. font-family: Cambria, Palatino Linotype, Palatino, Liberation Serif, serif;
  6. padding: 0;
  7. margin: 0;
  8. color: #111;
  9. }
  10. #spec-container {
  11. padding-left: 20px;
  12. flex-grow: 1;
  13. flex-basis: 66%;
  14. box-sizing: border-box;
  15. overflow: hidden;
  16. }
  17. body.oldtoc {
  18. margin: 0 auto;
  19. }
  20. a {
  21. text-decoration: none;
  22. color: #206ca7;
  23. }
  24. a:visited {
  25. color: #206ca7;
  26. }
  27. a:hover {
  28. text-decoration: underline;
  29. color: #239dee;
  30. }
  31. code {
  32. font-weight: bold;
  33. font-family: Consolas, Monaco, monospace;
  34. white-space: pre;
  35. }
  36. pre code {
  37. font-weight: inherit;
  38. }
  39. pre code.hljs {
  40. background-color: #fff;
  41. margin: 0;
  42. padding: 0;
  43. }
  44. ol.toc {
  45. list-style: none;
  46. padding-left: 0;
  47. }
  48. ol.toc ol.toc {
  49. padding-left: 2ex;
  50. list-style: none;
  51. }
  52. var {
  53. color: #2aa198;
  54. transition: background-color 0.25s ease;
  55. cursor: pointer;
  56. }
  57. var.referenced {
  58. background-color: #ffff33;
  59. }
  60. emu-const {
  61. font-family: sans-serif;
  62. }
  63. emu-val {
  64. font-weight: bold;
  65. }
  66. emu-alg ol, emu-alg ol ol ol ol {
  67. list-style-type: decimal;
  68. }
  69. emu-alg ol ol, emu-alg ol ol ol ol ol {
  70. list-style-type: lower-alpha;
  71. }
  72. emu-alg ol ol ol, ol ol ol ol ol ol {
  73. list-style-type: lower-roman;
  74. }
  75. emu-eqn {
  76. display: block;
  77. margin-left: 4em;
  78. }
  79. emu-eqn.inline {
  80. display: inline;
  81. margin: 0;
  82. }
  83. emu-eqn div:first-child {
  84. margin-left: -2em;
  85. }
  86. emu-note {
  87. margin: 1em 0;
  88. color: #666;
  89. border-left: 5px solid #ccc;
  90. display: flex;
  91. flex-direction: row;
  92. }
  93. emu-note > span.note {
  94. flex-basis: 100px;
  95. min-width: 100px;
  96. flex-grow: 0;
  97. flex-shrink: 1;
  98. text-transform: uppercase;
  99. padding-left: 5px;
  100. }
  101. emu-note[type=editor] {
  102. border-left-color: #faa;
  103. }
  104. emu-note > div.note-contents {
  105. flex-grow: 1;
  106. flex-shrink: 1;
  107. }
  108. emu-note > div.note-contents > p:first-child {
  109. margin-top: 0;
  110. }
  111. emu-note > div.note-contents > p:last-child {
  112. margin-bottom: 0;
  113. }
  114. emu-example {
  115. display: block;
  116. margin: 1em 3em;
  117. }
  118. emu-example figure figcaption {
  119. margin-top: 0.5em;
  120. text-align: left;
  121. }
  122. emu-production {
  123. display: block;
  124. margin-top: 1em;
  125. margin-bottom: 1em;
  126. margin-left: 5ex;
  127. }
  128. emu-grammar.inline, emu-production.inline,
  129. emu-grammar.inline emu-production emu-rhs, emu-production.inline emu-rhs {
  130. display: inline;
  131. }
  132. emu-grammar[collapsed] emu-production, emu-production[collapsed] {
  133. margin: 0;
  134. }
  135. emu-grammar[collapsed] emu-production emu-rhs, emu-production[collapsed] emu-rhs {
  136. display: inline;
  137. padding-left: 1ex;
  138. }
  139. emu-constraints {
  140. font-size: .75em;
  141. margin-right: 1ex;
  142. }
  143. emu-gann {
  144. margin-right: 1ex;
  145. }
  146. emu-gann emu-t:last-child,
  147. emu-gann emu-nt:last-child {
  148. margin-right: 0;
  149. }
  150. emu-geq {
  151. margin-left: 1ex;
  152. font-weight: bold;
  153. }
  154. emu-oneof {
  155. font-weight: bold;
  156. margin-left: 1ex;
  157. }
  158. emu-nt {
  159. display: inline-block;
  160. font-style: italic;
  161. white-space: nowrap;
  162. text-indent: 0;
  163. }
  164. emu-nt a, emu-nt a:visited {
  165. color: #333;
  166. }
  167. emu-rhs emu-nt {
  168. margin-right: 1ex;
  169. }
  170. emu-t {
  171. display: inline-block;
  172. font-family: monospace;
  173. font-weight: bold;
  174. white-space: nowrap;
  175. text-indent: 0;
  176. }
  177. emu-production emu-t {
  178. margin-right: 1ex;
  179. }
  180. emu-rhs {
  181. display: block;
  182. padding-left: 75px;
  183. text-indent: -25px;
  184. }
  185. emu-mods {
  186. font-size: .85em;
  187. vertical-align: sub;
  188. font-style: normal;
  189. font-weight: normal;
  190. }
  191. emu-production[collapsed] emu-mods {
  192. display: none;
  193. }
  194. emu-params, emu-opt {
  195. margin-right: 1ex;
  196. font-family: monospace;
  197. }
  198. emu-params, emu-constraints {
  199. color: #2aa198;
  200. }
  201. emu-opt {
  202. color: #b58900;
  203. }
  204. emu-gprose {
  205. font-size: 0.9em;
  206. font-family: Helvetica, Arial, sans-serif;
  207. }
  208. h1.shortname {
  209. color: #f60;
  210. font-size: 1.5em;
  211. margin: 0;
  212. }
  213. h1.version {
  214. color: #f60;
  215. font-size: 1.5em;
  216. margin: 0;
  217. }
  218. h1.title {
  219. margin-top: 0;
  220. color: #f60;
  221. }
  222. h1.first {
  223. margin-top: 0;
  224. }
  225. h1, h2, h3, h4, h5, h6 {
  226. position: relative;
  227. }
  228. h1 .secnum {
  229. text-decoration: none;
  230. margin-right: 10px;
  231. }
  232. h1 span.title {
  233. order: 2;
  234. }
  235. h1 { font-size: 2.67em; margin-top: 2em; margin-bottom: 1em; line-height: 1em;}
  236. h2 { font-size: 2em; }
  237. h3 { font-size: 1.56em; }
  238. h4 { font-size: 1.25em; }
  239. h5 { font-size: 1.11em; }
  240. h6 { font-size: 1em; }
  241. h1:hover span.utils {
  242. display: block;
  243. }
  244. span.utils {
  245. font-size: 18px;
  246. line-height: 18px;
  247. display: none;
  248. position: absolute;
  249. top: 100%;
  250. left: 0;
  251. right: 0;
  252. font-weight: normal;
  253. }
  254. span.utils:before {
  255. content: "⤷";
  256. display: inline-block;
  257. padding: 0 5px;
  258. }
  259. span.utils > * {
  260. display: inline-block;
  261. margin-right: 20px;
  262. }
  263. h1 span.utils span.anchor a,
  264. h2 span.utils span.anchor a,
  265. h3 span.utils span.anchor a,
  266. h4 span.utils span.anchor a,
  267. h5 span.utils span.anchor a,
  268. h6 span.utils span.anchor a {
  269. text-decoration: none;
  270. font-variant: small-caps;
  271. }
  272. h1 span.utils span.anchor a:hover,
  273. h2 span.utils span.anchor a:hover,
  274. h3 span.utils span.anchor a:hover,
  275. h4 span.utils span.anchor a:hover,
  276. h5 span.utils span.anchor a:hover,
  277. h6 span.utils span.anchor a:hover {
  278. color: #333;
  279. }
  280. emu-intro h1, emu-clause h1, emu-annex h1 { font-size: 2em; }
  281. emu-intro h2, emu-clause h2, emu-annex h2 { font-size: 1.56em; }
  282. emu-intro h3, emu-clause h3, emu-annex h3 { font-size: 1.25em; }
  283. emu-intro h4, emu-clause h4, emu-annex h4 { font-size: 1.11em; }
  284. emu-intro h5, emu-clause h5, emu-annex h5 { font-size: 1em; }
  285. emu-intro h6, emu-clause h6, emu-annex h6 { font-size: 0.9em; }
  286. emu-intro emu-intro h1, emu-clause emu-clause h1, emu-annex emu-annex h1 { font-size: 1.56em; }
  287. emu-intro emu-intro h2, emu-clause emu-clause h2, emu-annex emu-annex h2 { font-size: 1.25em; }
  288. emu-intro emu-intro h3, emu-clause emu-clause h3, emu-annex emu-annex h3 { font-size: 1.11em; }
  289. emu-intro emu-intro h4, emu-clause emu-clause h4, emu-annex emu-annex h4 { font-size: 1em; }
  290. emu-intro emu-intro h5, emu-clause emu-clause h5, emu-annex emu-annex h5 { font-size: 0.9em; }
  291. emu-intro emu-intro emu-intro h1, emu-clause emu-clause emu-clause h1, emu-annex emu-annex emu-annex h1 { font-size: 1.25em; }
  292. emu-intro emu-intro emu-intro h2, emu-clause emu-clause emu-clause h2, emu-annex emu-annex emu-annex h2 { font-size: 1.11em; }
  293. emu-intro emu-intro emu-intro h3, emu-clause emu-clause emu-clause h3, emu-annex emu-annex emu-annex h3 { font-size: 1em; }
  294. emu-intro emu-intro emu-intro h4, emu-clause emu-clause emu-clause h4, emu-annex emu-annex emu-annex h4 { font-size: 0.9em; }
  295. emu-intro emu-intro emu-intro emu-intro h1, emu-clause emu-clause emu-clause emu-clause h1, emu-annex emu-annex emu-annex emu-annex h1 { font-size: 1.11em; }
  296. emu-intro emu-intro emu-intro emu-intro h2, emu-clause emu-clause emu-clause emu-clause h2, emu-annex emu-annex emu-annex emu-annex h2 { font-size: 1em; }
  297. emu-intro emu-intro emu-intro emu-intro h3, emu-clause emu-clause emu-clause emu-clause h3, emu-annex emu-annex emu-annex emu-annex h3 { font-size: 0.9em; }
  298. emu-intro emu-intro emu-intro emu-intro emu-intro h1, emu-clause emu-clause emu-clause emu-clause emu-clause h1, emu-annex emu-annex emu-annex emu-annex emu-annex h1 { font-size: 1em; }
  299. emu-intro emu-intro emu-intro emu-intro emu-intro h2, emu-clause emu-clause emu-clause emu-clause emu-clause h2, emu-annex emu-annex emu-annex emu-annex emu-annex h2 { font-size: 0.9em; }
  300. emu-intro emu-intro emu-intro emu-intro emu-intro emu-intro h1, emu-clause emu-clause emu-clause emu-clause emu-clause emu-clause h1, emu-annex emu-annex emu-annex emu-annex emu-annex emu-annex h1 { font-size: 0.9em }
  301. emu-clause {
  302. display: block;
  303. }
  304. /* Figures and tables */
  305. figure { display: block; margin: 1em 0 3em 0; }
  306. figure object { display: block; margin: 0 auto; }
  307. figure table.real-table { margin: 0 auto; }
  308. figure figcaption {
  309. display: block;
  310. color: #555555;
  311. font-weight: bold;
  312. text-align: center;
  313. }
  314. emu-table table {
  315. margin: 0 auto;
  316. }
  317. emu-table table, table.real-table {
  318. border-collapse: collapse;
  319. }
  320. emu-table td, emu-table th, table.real-table td, table.real-table th {
  321. border: 1px solid black;
  322. padding: 0.4em;
  323. vertical-align: baseline;
  324. }
  325. emu-table th, emu-table thead td, table.real-table th {
  326. background-color: #eeeeee;
  327. }
  328. /* Note: the left content edges of table.lightweight-table >tbody >tr >td
  329. and div.display line up. */
  330. table.lightweight-table {
  331. border-collapse: collapse;
  332. margin: 0 0 0 1.5em;
  333. }
  334. table.lightweight-table td, table.lightweight-table th {
  335. border: none;
  336. padding: 0 0.5em;
  337. vertical-align: baseline;
  338. }
  339. /* diff styles */
  340. ins {
  341. background-color: #e0f8e0;
  342. text-decoration: none;
  343. border-bottom: 1px solid #396;
  344. }
  345. del {
  346. background-color: #fee;
  347. }
  348. ins.block, del.block,
  349. emu-production > ins, emu-production > del,
  350. emu-grammar > ins, emu-grammar > del {
  351. display: block;
  352. }
  353. /* Menu Styles */
  354. #menu-toggle {
  355. font-size: 2em;
  356. position: fixed;
  357. top: 0;
  358. left: 0;
  359. width: 1.5em;
  360. height: 1.5em;
  361. z-index: 3;
  362. visibility: hidden;
  363. color: #1567a2;
  364. background-color: #fff;
  365. line-height: 1.5em;
  366. text-align: center;
  367. -webkit-touch-callout: none;
  368. -webkit-user-select: none;
  369. -khtml-user-select: none;
  370. -moz-user-select: none;
  371. -ms-user-select: none;
  372. user-select: none;;
  373. cursor: pointer;
  374. }
  375. #menu {
  376. display: flex;
  377. flex-direction: column;
  378. width: 33%; height: 100vh;
  379. max-width: 500px;
  380. box-sizing: border-box;
  381. background-color: #ddd;
  382. overflow: hidden;
  383. transition: opacity 0.1s linear;
  384. padding: 0 5px;
  385. position: fixed;
  386. left: 0; top: 0;
  387. z-index: 2;
  388. }
  389. #menu-spacer {
  390. flex-basis: 33%;
  391. max-width: 500px;
  392. flex-grow: 0;
  393. flex-shrink: 0;
  394. }
  395. #menu a {
  396. color: #1567a2;
  397. }
  398. #menu.active {
  399. display: flex;
  400. opacity: 1;
  401. z-index: 2;
  402. }
  403. #menu-pins {
  404. flex-grow: 1;
  405. display: none;
  406. }
  407. #menu-pins.active {
  408. display: block;
  409. }
  410. #menu-pins-list {
  411. margin: 0;
  412. padding: 0;
  413. counter-reset: pins-counter;
  414. }
  415. #menu-pins-list > li:before {
  416. content: counter(pins-counter);
  417. counter-increment: pins-counter;
  418. display: inline-block;
  419. width: 25px;
  420. text-align: center;
  421. border: 1px solid #bbb;
  422. padding: 2px;
  423. margin: 4px;
  424. box-sizing: border-box;
  425. line-height: 1em;
  426. background-color: #ccc;
  427. border-radius: 4px;
  428. }
  429. #menu-toc > ol {
  430. padding: 0;
  431. flex-grow: 1;
  432. }
  433. #menu-toc > ol li {
  434. padding: 0;
  435. }
  436. #menu-toc > ol , #menu-toc > ol ol {
  437. list-style-type: none;
  438. margin: 0;
  439. padding: 0;
  440. }
  441. #menu-toc > ol ol {
  442. padding-left: 0.75em;
  443. }
  444. #menu-toc li {
  445. text-overflow: ellipsis;
  446. overflow: hidden;
  447. white-space: nowrap;
  448. }
  449. #menu-toc .item-toggle {
  450. display: inline-block;
  451. transform: rotate(-45deg) translate(-5px, -5px);
  452. transition: transform 0.1s ease;
  453. text-align: center;
  454. width: 20px;
  455. color: #aab;
  456. -webkit-touch-callout: none;
  457. -webkit-user-select: none;
  458. -khtml-user-select: none;
  459. -moz-user-select: none;
  460. -ms-user-select: none;
  461. user-select: none;;
  462. cursor: pointer;
  463. }
  464. #menu-toc .item-toggle-none {
  465. display: inline-block;
  466. width: 20px;
  467. }
  468. #menu-toc li.active > .item-toggle {
  469. transform: rotate(45deg) translate(-5px, -5px);
  470. }
  471. #menu-toc li > ol {
  472. display: none;
  473. }
  474. #menu-toc li.active > ol {
  475. display: block;
  476. }
  477. #menu-toc li.revealed > a {
  478. background-color: #bbb;
  479. font-weight: bold;
  480. /*
  481. background-color: #222;
  482. color: #c6d8e4;
  483. */
  484. }
  485. #menu-toc li.revealed-leaf> a {
  486. color: #206ca7;
  487. /*
  488. background-color: #222;
  489. color: #c6d8e4;
  490. */
  491. }
  492. #menu-toc li.revealed > .item-toggle {
  493. transform: rotate(45deg) translate(-5px, -5px);
  494. }
  495. #menu-toc li.revealed > ol {
  496. display: block;
  497. }
  498. #menu-toc li > a {
  499. padding: 2px 5px;
  500. }
  501. #menu > * {
  502. margin-bottom: 5px;
  503. }
  504. .menu-pane-header {
  505. padding: 0 5px;
  506. text-transform: uppercase;
  507. background-color: #aaa;
  508. color: #335;
  509. font-weight: bold;
  510. letter-spacing: 2px;
  511. flex-grow: 0;
  512. flex-shrink: 0;
  513. font-size: 0.8em;
  514. }
  515. #menu-toc {
  516. display: flex;
  517. flex-direction: column;
  518. width: 100%;
  519. overflow: hidden;
  520. flex-grow: 1;
  521. }
  522. #menu-toc ol.toc {
  523. overflow-x: hidden;
  524. overflow-y: auto;
  525. }
  526. #menu-search {
  527. position: relative;
  528. flex-grow: 0;
  529. flex-shrink: 0;
  530. width: 100%;
  531. display: flex;
  532. flex-direction: column;
  533. max-height: 300px;
  534. }
  535. #menu-trace-list {
  536. display: none;
  537. }
  538. #menu-search-box {
  539. box-sizing: border-box;
  540. display: block;
  541. width: 100%;
  542. margin: 5px 0 0 0;
  543. font-size: 1em;
  544. padding: 2px;
  545. background-color: #bbb;
  546. border: 1px solid #999;
  547. }
  548. #menu-search-results {
  549. overflow-x: hidden;
  550. overflow-y: auto;
  551. }
  552. li.menu-search-result-clause:before {
  553. content: 'clause';
  554. width: 40px;
  555. display: inline-block;
  556. text-align: right;
  557. padding-right: 1ex;
  558. color: #666;
  559. font-size: 75%;
  560. }
  561. li.menu-search-result-op:before {
  562. content: 'op';
  563. width: 40px;
  564. display: inline-block;
  565. text-align: right;
  566. padding-right: 1ex;
  567. color: #666;
  568. font-size: 75%;
  569. }
  570. li.menu-search-result-prod:before {
  571. content: 'prod';
  572. width: 40px;
  573. display: inline-block;
  574. text-align: right;
  575. padding-right: 1ex;
  576. color: #666;
  577. font-size: 75%
  578. }
  579. li.menu-search-result-term:before {
  580. content: 'term';
  581. width: 40px;
  582. display: inline-block;
  583. text-align: right;
  584. padding-right: 1ex;
  585. color: #666;
  586. font-size: 75%
  587. }
  588. #menu-search-results ul {
  589. padding: 0 5px;
  590. margin: 0;
  591. }
  592. #menu-search-results li {
  593. white-space: nowrap;
  594. text-overflow: ellipsis;
  595. }
  596. #menu-trace-list {
  597. counter-reset: item;
  598. margin: 0 0 0 20px;
  599. padding: 0;
  600. }
  601. #menu-trace-list li {
  602. display: block;
  603. white-space: nowrap;
  604. }
  605. #menu-trace-list li .secnum:after {
  606. content: " ";
  607. }
  608. #menu-trace-list li:before {
  609. content: counter(item) " ";
  610. background-color: #222;
  611. counter-increment: item;
  612. color: #999;
  613. width: 20px;
  614. height: 20px;
  615. line-height: 20px;
  616. display: inline-block;
  617. text-align: center;
  618. margin: 2px 4px 2px 0;
  619. }
  620. @media (max-width: 1000px) {
  621. body {
  622. margin: 0;
  623. display: block;
  624. }
  625. #menu {
  626. display: none;
  627. padding-top: 3em;
  628. width: 450px;
  629. }
  630. #menu.active {
  631. position: fixed;
  632. height: 100%;
  633. left: 0;
  634. top: 0;
  635. right: 300px;
  636. }
  637. #menu-toggle {
  638. visibility: visible;
  639. }
  640. #spec-container {
  641. padding: 0 5px;
  642. }
  643. }
  644. @media only screen and (max-width: 800px) {
  645. #menu {
  646. width: 100%;
  647. }
  648. h1 .secnum:empty {
  649. margin: 0; padding: 0;
  650. }
  651. }