blob: 6fa1a1d78e18e69417778edfb3f372cfb17299c0 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
|
<html>
<head>
<meta charset="utf-8">
<title>Dotty - {{ page.title }}</title>
<link rel="shortcut icon" type="image/png" href="{{ site.baseurl}}/images/favicon.png"/>
<link rel="stylesheet" href="http://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.7.0/styles/github.min.css">
<link rel="stylesheet" href="{{ site.baseurl }}/css/main.css">
</head>
<body>
<div id="container">
<a class="logo-container" href="{{ site.baseurl }}/">
<div id="scala-logo-mobile">
{% include scala-logo.html %}
</div>
</a>
<div id="content">
<h1>{{ page.title }}</h1>
<div class="edit-docs">
<a href="{{site.repository_url}}/edit/master/docs/{{page.path}}">[edit on github]</a>
</div>
{{ content }}
</div>
<div id="toc">
{% include toc.html %}
</div>
</div>
</body>
<script src="https://cdnjs.cloudflare.com/ajax/libs/mark.js/8.4.0/mark.min.js"></script>
<script src="{{ site.baseurl }}/js/highlight.pack.js"></script>
<script language="javascript">
hljs.initHighlightingOnLoad();
var x = document.links.length;
for (i = 0; i < x; i++) {
var thisHREF = document.links[i].href;
if (thisHREF.indexOf(window.location.hostname) > -1) thisHREF = thisHREF.replace(".md",".html")
document.links[i].setAttribute('href', thisHREF);
}
function getQueryVariable(variable) {
var query = window.location.search.substring(1);
var vars = query.split('&');
for (var i = 0; i < vars.length; i++) {
var pair = vars[i].split('=');
if (pair[0] === variable) {
return decodeURIComponent(pair[1].replace(/\+/g, '%20'));
}
}
}
var highlight = getQueryVariable("highlight");
if (highlight) {
var context = document.querySelector("#content");
var instance = new Mark(context);
instance.mark(highlight);
}
</script>
</html>
|
