header.html.inc (91 lines of code) (raw):

<html> <head> <title>Effective Scala</title> <meta http-equiv="Content-Type" content="text/html; charset=utf-8"> <script type="text/javascript" src="https://use.typekit.com/bub8efs.js"></script> <script type="text/javascript">try{Typekit.load();}catch(e){}</script> <script> (function(i,s,o,g,r,a,m){i['GoogleAnalyticsObject']=r;i[r]=i[r]||function(){ (i[r].q=i[r].q||[]).push(arguments)},i[r].l=1*new Date();a=s.createElement(o), m=s.getElementsByTagName(o)[0];a.async=1;a.src=g;m.parentNode.insertBefore(a,m) })(window,document,'script','//www.google-analytics.com/analytics.js','ga'); ga('create', 'UA-39101739-8', 'twitter.github.io'); ga('send', 'pageview'); </script> <!-- <link href='https://fonts.googleapis.com/css?family=Droid+Sans+Mono' rel='stylesheet' type='text/css'> <link href='https://fonts.googleapis.com/css?family=Droid+Serif' rel='stylesheet' type='text/css'> <link href='https://fonts.googleapis.com/css?family=Droid+Sans' rel='stylesheet' type='text/css'> <link href='https://fonts.googleapis.com/css?family=Inconsolata' rel='stylesheet' type='text/css'> --> <link href='https://fonts.googleapis.com/css?family=Droid+Sans+Mono' rel='stylesheet' type='text/css'> <style> body { font-family: "ff-meta-serif-web-pro", Georgia, serif; text-rendering: optimizeLegibility; font-size: 17px; margin: 0 1.0in 0 1.0in; /* line-height: 1.3em;*/ } address { text-align: center; } .header { text-align: center; margin-top: 1em; } .rhs { text-align: left; } p { text-indent: 1em; text-align: justify; } .LP { text-indent: 0em; } code { font-family: "Droid Sans Mono'", monospace; /* font-size: 0.75em;*/ font-size: 0.80em; } address { font-family: sans-serif; } h1 { font-family: "proxima-nova"; } h2 { font-weight: bold; font-size: 110%; margin-top: 1.5em; margin-bottom: 0.05in; } h3 { font-size: 100%; font-style: oblique; margin-top: 1.5em; margin-bottom: 0.05in; } pre { margin: 0 0.5in 0 0.5in; } dl.rules dt { font-style: oblique; } table#toc { margin: 0 auto; } /* XXX: apply only to TOC. todo: reapply -- html whatever? */ ul { /* list-style-type: none;*/ } .algo { font-variant: small-caps; } div.explainer { margin-left: 3em; border-left: 2px solid; padding-left: 1em; } .explainer > h3 { margin-top: 0px; font-style: normal; } .footer { font-style: oblique; font-size: small; } </style> </head> <body>