You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

773 lines
12 KiB

8 years ago
  1. body {
  2. margin: 0;
  3. font-family: Arial, sans-serif;
  4. font-size: 16px;
  5. background-color: #fff;
  6. line-height: 1.3em;
  7. }
  8. pre,
  9. code {
  10. font-family: Menlo, monospace;
  11. font-size: 14px;
  12. }
  13. pre {
  14. line-height: 1.4em;
  15. overflow-x: auto;
  16. }
  17. pre .comment {
  18. color: #006600;
  19. }
  20. pre .highlight,
  21. pre .highlight-comment,
  22. pre .selection-highlight,
  23. pre .selection-highlight-comment {
  24. background: #FFFF00;
  25. }
  26. pre .selection,
  27. pre .selection-comment {
  28. background: #FF9632;
  29. }
  30. pre .ln {
  31. color: #999;
  32. }
  33. body {
  34. color: #222;
  35. }
  36. a,
  37. .exampleHeading .text {
  38. color: #375EAB;
  39. text-decoration: none;
  40. }
  41. a:hover,
  42. .exampleHeading .text:hover {
  43. text-decoration: underline;
  44. }
  45. p, li {
  46. max-width: 800px;
  47. word-wrap: break-word;
  48. }
  49. p,
  50. pre,
  51. ul,
  52. ol {
  53. margin: 20px;
  54. }
  55. pre {
  56. background: #EFEFEF;
  57. padding: 10px;
  58. -webkit-border-radius: 5px;
  59. -moz-border-radius: 5px;
  60. border-radius: 5px;
  61. }
  62. h1,
  63. h2,
  64. h3,
  65. h4,
  66. .rootHeading {
  67. margin: 20px 0 20px;
  68. padding: 0;
  69. color: #375EAB;
  70. font-weight: bold;
  71. }
  72. h1 {
  73. font-size: 28px;
  74. line-height: 1;
  75. }
  76. h2 {
  77. font-size: 20px;
  78. background: #E0EBF5;
  79. padding: 8px;
  80. line-height: 1.25;
  81. font-weight: normal;
  82. }
  83. h2 a {
  84. font-weight: bold;
  85. }
  86. h3 {
  87. font-size: 20px;
  88. }
  89. h3,
  90. h4 {
  91. margin: 20px 5px;
  92. }
  93. h4 {
  94. font-size: 16px;
  95. }
  96. .rootHeading {
  97. font-size: 20px;
  98. margin: 0;
  99. }
  100. dl {
  101. margin: 20px;
  102. }
  103. dd {
  104. margin: 0 0 0 20px;
  105. }
  106. dl,
  107. dd {
  108. font-size: 14px;
  109. }
  110. div#nav table td {
  111. vertical-align: top;
  112. }
  113. .pkg-dir {
  114. padding: 0 10px;
  115. }
  116. .pkg-dir table {
  117. border-collapse: collapse;
  118. border-spacing: 0;
  119. }
  120. .pkg-name {
  121. padding-right: 10px;
  122. }
  123. .alert {
  124. color: #AA0000;
  125. }
  126. .top-heading {
  127. float: left;
  128. padding: 21px 0;
  129. font-size: 20px;
  130. font-weight: normal;
  131. }
  132. .top-heading a {
  133. color: #222;
  134. text-decoration: none;
  135. }
  136. div#topbar {
  137. background: #E0EBF5;
  138. height: 64px;
  139. overflow: hidden;
  140. }
  141. body {
  142. text-align: center;
  143. }
  144. div#page {
  145. width: 100%;
  146. }
  147. div#page > .container,
  148. div#topbar > .container {
  149. text-align: left;
  150. margin-left: auto;
  151. margin-right: auto;
  152. padding: 0 20px;
  153. }
  154. div#topbar > .container,
  155. div#page > .container {
  156. max-width: 950px;
  157. }
  158. div#page.wide > .container,
  159. div#topbar.wide > .container {
  160. max-width: none;
  161. }
  162. div#plusone {
  163. float: right;
  164. clear: right;
  165. margin-top: 5px;
  166. }
  167. div#footer {
  168. text-align: center;
  169. color: #666;
  170. font-size: 14px;
  171. margin: 40px 0;
  172. }
  173. div#menu > a,
  174. div#menu > input,
  175. div#learn .buttons a,
  176. div.play .buttons a,
  177. div#blog .read a,
  178. #menu-button {
  179. padding: 10px;
  180. text-decoration: none;
  181. font-size: 16px;
  182. -webkit-border-radius: 5px;
  183. -moz-border-radius: 5px;
  184. border-radius: 5px;
  185. }
  186. div#playground .buttons a,
  187. div#menu > a,
  188. div#menu > input,
  189. #menu-button {
  190. border: 1px solid #375EAB;
  191. }
  192. div#playground .buttons a,
  193. div#menu > a,
  194. #menu-button {
  195. color: white;
  196. background: #375EAB;
  197. }
  198. #playgroundButton.active {
  199. background: white;
  200. color: #375EAB;
  201. }
  202. a#start,
  203. div#learn .buttons a,
  204. div.play .buttons a,
  205. div#blog .read a {
  206. color: #222;
  207. border: 1px solid #375EAB;
  208. background: #E0EBF5;
  209. }
  210. .download {
  211. width: 150px;
  212. }
  213. div#menu {
  214. text-align: right;
  215. padding: 10px;
  216. white-space: nowrap;
  217. max-height: 0;
  218. -moz-transition: max-height .25s linear;
  219. transition: max-height .25s linear;
  220. width: 100%;
  221. }
  222. div#menu.menu-visible {
  223. max-height: 500px;
  224. }
  225. div#menu > a,
  226. #menu-button {
  227. margin: 10px 2px;
  228. padding: 10px;
  229. }
  230. div#menu > input {
  231. position: relative;
  232. top: 1px;
  233. width: 140px;
  234. background: white;
  235. color: #222;
  236. box-sizing: border-box;
  237. }
  238. div#menu > input.inactive {
  239. color: #999;
  240. }
  241. #menu-button {
  242. display: none;
  243. position: absolute;
  244. right: 5px;
  245. top: 0;
  246. margin-right: 5px;
  247. }
  248. #menu-button-arrow {
  249. display: inline-block;
  250. }
  251. .vertical-flip {
  252. transform: rotate(-180deg);
  253. }
  254. div.left {
  255. float: left;
  256. clear: left;
  257. margin-right: 2.5%;
  258. }
  259. div.right {
  260. float: right;
  261. clear: right;
  262. margin-left: 2.5%;
  263. }
  264. div.left,
  265. div.right {
  266. width: 45%;
  267. }
  268. div#learn,
  269. div#about {
  270. padding-top: 20px;
  271. }
  272. div#learn h2,
  273. div#about {
  274. margin: 0;
  275. }
  276. div#about {
  277. font-size: 20px;
  278. margin: 0 auto 30px;
  279. }
  280. div#gopher {
  281. background: url(http://localhost:6060/doc/gopher/frontpage.png) no-repeat;
  282. background-position: center top;
  283. height: 155px;
  284. }
  285. a#start {
  286. display: block;
  287. padding: 10px;
  288. text-align: center;
  289. text-decoration: none;
  290. -webkit-border-radius: 5px;
  291. -moz-border-radius: 5px;
  292. border-radius: 5px;
  293. }
  294. a#start .big {
  295. display: block;
  296. font-weight: bold;
  297. font-size: 20px;
  298. }
  299. a#start .desc {
  300. display: block;
  301. font-size: 14px;
  302. font-weight: normal;
  303. margin-top: 5px;
  304. }
  305. div#learn .popout {
  306. float: right;
  307. display: block;
  308. cursor: pointer;
  309. font-size: 12px;
  310. background: url(http://localhost:6060/doc/share.png) no-repeat;
  311. background-position: right top;
  312. padding: 5px 27px;
  313. }
  314. div#learn pre,
  315. div#learn textarea {
  316. padding: 0;
  317. margin: 0;
  318. font-family: Menlo, monospace;
  319. font-size: 14px;
  320. }
  321. div#learn .input {
  322. padding: 10px;
  323. margin-top: 10px;
  324. height: 150px;
  325. -webkit-border-top-left-radius: 5px;
  326. -webkit-border-top-right-radius: 5px;
  327. -moz-border-radius-topleft: 5px;
  328. -moz-border-radius-topright: 5px;
  329. border-top-left-radius: 5px;
  330. border-top-right-radius: 5px;
  331. }
  332. div#learn .input textarea {
  333. width: 100%;
  334. height: 100%;
  335. border: none;
  336. outline: none;
  337. resize: none;
  338. }
  339. div#learn .output {
  340. border-top: none !important;
  341. padding: 10px;
  342. height: 59px;
  343. overflow: auto;
  344. -webkit-border-bottom-right-radius: 5px;
  345. -webkit-border-bottom-left-radius: 5px;
  346. -moz-border-radius-bottomright: 5px;
  347. -moz-border-radius-bottomleft: 5px;
  348. border-bottom-right-radius: 5px;
  349. border-bottom-left-radius: 5px;
  350. }
  351. div#learn .output pre {
  352. padding: 0;
  353. -webkit-border-radius: 0;
  354. -moz-border-radius: 0;
  355. border-radius: 0;
  356. }
  357. div#learn .input,
  358. div#learn .input textarea,
  359. div#learn .output,
  360. div#learn .output pre {
  361. background: #FFFFD8;
  362. }
  363. div#learn .input,
  364. div#learn .output {
  365. border: 1px solid #375EAB;
  366. }
  367. div#learn .buttons {
  368. float: right;
  369. padding: 20px 0 10px 0;
  370. text-align: right;
  371. }
  372. div#learn .buttons a {
  373. height: 16px;
  374. margin-left: 5px;
  375. padding: 10px;
  376. }
  377. div#learn .toys {
  378. margin-top: 8px;
  379. }
  380. div#learn .toys select {
  381. border: 1px solid #375EAB;
  382. margin: 0;
  383. }
  384. div#learn .output .exit {
  385. display: none;
  386. }
  387. div#video {
  388. max-width: 100%;
  389. }
  390. div#blog,
  391. div#video {
  392. margin-top: 40px;
  393. }
  394. div#blog > a,
  395. div#blog > div,
  396. div#blog > h2,
  397. div#video > a,
  398. div#video > div,
  399. div#video > h2 {
  400. margin-bottom: 10px;
  401. }
  402. div#blog .title,
  403. div#video .title {
  404. display: block;
  405. font-size: 20px;
  406. }
  407. div#blog .when {
  408. color: #666;
  409. font-size: 14px;
  410. }
  411. div#blog .read {
  412. text-align: right;
  413. }
  414. .toggleButton { cursor: pointer; }
  415. .toggle .collapsed { display: block; }
  416. .toggle .expanded { display: none; }
  417. .toggleVisible .collapsed { display: none; }
  418. .toggleVisible .expanded { display: block; }
  419. table.codetable { margin-left: auto; margin-right: auto; border-style: none; }
  420. table.codetable td { padding-right: 10px; }
  421. hr { border-style: none; border-top: 1px solid black; }
  422. img.gopher {
  423. float: right;
  424. margin-left: 10px;
  425. margin-bottom: 10px;
  426. z-index: -1;
  427. }
  428. h2 { clear: right; }
  429. /* example and drop-down playground */
  430. div.play {
  431. padding: 0 20px 40px 20px;
  432. }
  433. div.play pre,
  434. div.play textarea,
  435. div.play .lines {
  436. padding: 0;
  437. margin: 0;
  438. font-family: Menlo, monospace;
  439. font-size: 14px;
  440. }
  441. div.play .input {
  442. padding: 10px;
  443. margin-top: 10px;
  444. -webkit-border-top-left-radius: 5px;
  445. -webkit-border-top-right-radius: 5px;
  446. -moz-border-radius-topleft: 5px;
  447. -moz-border-radius-topright: 5px;
  448. border-top-left-radius: 5px;
  449. border-top-right-radius: 5px;
  450. overflow: hidden;
  451. }
  452. div.play .input textarea {
  453. width: 100%;
  454. height: 100%;
  455. border: none;
  456. outline: none;
  457. resize: none;
  458. overflow: hidden;
  459. }
  460. div#playground .input textarea {
  461. overflow: auto;
  462. resize: auto;
  463. }
  464. div.play .output {
  465. border-top: none !important;
  466. padding: 10px;
  467. max-height: 200px;
  468. overflow: auto;
  469. -webkit-border-bottom-right-radius: 5px;
  470. -webkit-border-bottom-left-radius: 5px;
  471. -moz-border-radius-bottomright: 5px;
  472. -moz-border-radius-bottomleft: 5px;
  473. border-bottom-right-radius: 5px;
  474. border-bottom-left-radius: 5px;
  475. }
  476. div.play .output pre {
  477. padding: 0;
  478. -webkit-border-radius: 0;
  479. -moz-border-radius: 0;
  480. border-radius: 0;
  481. }
  482. div.play .input,
  483. div.play .input textarea,
  484. div.play .output,
  485. div.play .output pre {
  486. background: #FFFFD8;
  487. }
  488. div.play .input,
  489. div.play .output {
  490. border: 1px solid #375EAB;
  491. }
  492. div.play .buttons {
  493. float: right;
  494. padding: 20px 0 10px 0;
  495. text-align: right;
  496. }
  497. div.play .buttons a {
  498. height: 16px;
  499. margin-left: 5px;
  500. padding: 10px;
  501. cursor: pointer;
  502. }
  503. .output .stderr {
  504. color: #933;
  505. }
  506. .output .system {
  507. color: #999;
  508. }
  509. /* drop-down playground */
  510. #playgroundButton,
  511. div#playground {
  512. /* start hidden; revealed by javascript */
  513. display: none;
  514. }
  515. div#playground {
  516. position: absolute;
  517. top: 63px;
  518. right: 20px;
  519. padding: 0 10px 10px 10px;
  520. z-index: 1;
  521. text-align: left;
  522. background: #E0EBF5;
  523. border: 1px solid #B0BBC5;
  524. border-top: none;
  525. -webkit-border-bottom-left-radius: 5px;
  526. -webkit-border-bottom-right-radius: 5px;
  527. -moz-border-radius-bottomleft: 5px;
  528. -moz-border-radius-bottomright: 5px;
  529. border-bottom-left-radius: 5px;
  530. border-bottom-right-radius: 5px;
  531. }
  532. div#playground .code {
  533. width: 520px;
  534. height: 200px;
  535. }
  536. div#playground .output {
  537. height: 100px;
  538. }
  539. /* Inline runnable snippets (play.js/initPlayground) */
  540. #content .code pre, #content .playground pre, #content .output pre {
  541. margin: 0;
  542. padding: 0;
  543. background: none;
  544. border: none;
  545. outline: 0px solid transparent;
  546. overflow: auto;
  547. }
  548. #content .playground .number, #content .code .number {
  549. color: #999;
  550. }
  551. #content .code, #content .playground, #content .output {
  552. width: auto;
  553. margin: 20px;
  554. padding: 10px;
  555. -webkit-border-radius: 5px;
  556. -moz-border-radius: 5px;
  557. border-radius: 5px;
  558. }
  559. #content .code, #content .playground {
  560. background: #e9e9e9;
  561. }
  562. #content .output {
  563. background: #202020;
  564. }
  565. #content .output .stdout, #content .output pre {
  566. color: #e6e6e6;
  567. }
  568. #content .output .stderr, #content .output .error {
  569. color: rgb(244, 74, 63);
  570. }
  571. #content .output .system, #content .output .exit {
  572. color: rgb(255, 209, 77)
  573. }
  574. #content .buttons {
  575. position: relative;
  576. float: right;
  577. top: -50px;
  578. right: 30px;
  579. }
  580. #content .output .buttons {
  581. top: -60px;
  582. right: 0;
  583. height: 0;
  584. }
  585. #content .buttons .kill {
  586. display: none;
  587. visibility: hidden;
  588. }
  589. a.error {
  590. font-weight: bold;
  591. color: white;
  592. background-color: darkred;
  593. border-bottom-left-radius: 4px;
  594. border-bottom-right-radius: 4px;
  595. border-top-left-radius: 4px;
  596. border-top-right-radius: 4px;
  597. padding: 2px 4px 2px 4px; /* TRBL */
  598. }
  599. #heading-narrow {
  600. display: none;
  601. }
  602. .downloading {
  603. background: #F9F9BE;
  604. padding: 10px;
  605. text-align: center;
  606. border-radius: 5px;
  607. }
  608. @media (max-width: 930px) {
  609. #heading-wide {
  610. display: none;
  611. }
  612. #heading-narrow {
  613. display: block;
  614. }
  615. }
  616. @media (max-width: 760px) {
  617. .container .left,
  618. .container .right {
  619. width: auto;
  620. float: none;
  621. }
  622. div#about {
  623. max-width: 500px;
  624. text-align: center;
  625. }
  626. }
  627. @media (min-width: 700px) and (max-width: 1000px) {
  628. div#menu > a {
  629. margin: 5px 0;
  630. font-size: 14px;
  631. }
  632. div#menu > input {
  633. font-size: 14px;
  634. }
  635. }
  636. @media (max-width: 700px) {
  637. body {
  638. font-size: 15px;
  639. }
  640. pre,
  641. code {
  642. font-size: 13px;
  643. }
  644. div#page > .container {
  645. padding: 0 10px;
  646. }
  647. div#topbar {
  648. height: auto;
  649. padding: 10px;
  650. }
  651. div#topbar > .container {
  652. padding: 0;
  653. }
  654. #heading-wide {
  655. display: block;
  656. }
  657. #heading-narrow {
  658. display: none;
  659. }
  660. .top-heading {
  661. float: none;
  662. display: inline-block;
  663. padding: 12px;
  664. }
  665. div#menu {
  666. padding: 0;
  667. min-width: 0;
  668. text-align: left;
  669. float: left;
  670. }
  671. div#menu > a,
  672. div#menu > input {
  673. display: block;
  674. margin-left: 0;
  675. margin-right: 0;
  676. }
  677. div#menu > input {
  678. width: 100%;
  679. }
  680. #menu-button {
  681. display: inline-block;
  682. }
  683. p,
  684. pre,
  685. ul,
  686. ol {
  687. margin: 10px;
  688. }
  689. .pkg-synopsis {
  690. display: none;
  691. }
  692. img.gopher {
  693. display: none;
  694. }
  695. }
  696. @media (max-width: 480px) {
  697. #heading-wide {
  698. display: none;
  699. }
  700. #heading-narrow {
  701. display: block;
  702. }
  703. }
  704. @media print {
  705. pre {
  706. background: #FFF;
  707. border: 1px solid #BBB;
  708. white-space: pre-wrap;
  709. }
  710. }