diff options
| author | Felix Mulder <felix.mulder@gmail.com> | 2016-11-07 17:37:07 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2016-11-07 17:37:07 +0100 |
| commit | d1e0d3bc7096022d03928b78c33f9ffabae16aa5 (patch) | |
| tree | e5553b111aef328b5cc71909f6978cf0b5401c23 /docs/_layouts | |
| parent | 5d590242132b0f38fc04afed2c787dadfd8d6c2f (diff) | |
| parent | e0c1d1665c8100ccad6c324e8e15e38df9b39327 (diff) | |
| download | dotty-d1e0d3bc7096022d03928b78c33f9ffabae16aa5.tar.gz dotty-d1e0d3bc7096022d03928b78c33f9ffabae16aa5.tar.bz2 dotty-d1e0d3bc7096022d03928b78c33f9ffabae16aa5.zip | |
Merge pull request #1676 from felixmulder/topic/docs-add-search
Fix a number of doc issues
Diffstat (limited to 'docs/_layouts')
| -rw-r--r-- | docs/_layouts/blog.html | 3 | ||||
| -rw-r--r-- | docs/_layouts/default.html | 26 | ||||
| -rw-r--r-- | docs/_layouts/search.html | 17 |
3 files changed, 44 insertions, 2 deletions
diff --git a/docs/_layouts/blog.html b/docs/_layouts/blog.html index 560b8a64c..f476bf5fa 100644 --- a/docs/_layouts/blog.html +++ b/docs/_layouts/blog.html @@ -2,12 +2,11 @@ layout: default --- -<h1 class="title">{{ page.title }}</h1> <h2 class="subtitle">{{ page.subTitle }}</h2> <div class="author-container {% if page.authorImg != null %} spaced {% endif %}"> {% if page.authorImg != null %} - <img src="{{ site.baseurl }}/{{ page.authorImg }}"/> + <img src="{{ site.baseurl }}{{ page.authorImg }}"/> {% endif %} <div class="author-info"> <div>{{ page.author }}</div> diff --git a/docs/_layouts/default.html b/docs/_layouts/default.html index ce1345145..6fa1a1d78 100644 --- a/docs/_layouts/default.html +++ b/docs/_layouts/default.html @@ -15,6 +15,10 @@ </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"> @@ -22,6 +26,7 @@ </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(); @@ -31,5 +36,26 @@ 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> diff --git a/docs/_layouts/search.html b/docs/_layouts/search.html new file mode 100644 index 000000000..14994ab62 --- /dev/null +++ b/docs/_layouts/search.html @@ -0,0 +1,17 @@ +<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"> + <div class="search"> + {{ content }} + </div> + </div> + </body> +</html> |