diff options
author | Felix Mulder <felix.mulder@gmail.com> | 2016-11-07 17:29:50 +0100 |
---|---|---|
committer | Felix Mulder <felix.mulder@gmail.com> | 2016-11-07 17:29:50 +0100 |
commit | e0c1d1665c8100ccad6c324e8e15e38df9b39327 (patch) | |
tree | e5553b111aef328b5cc71909f6978cf0b5401c23 /docs/_layouts | |
parent | f179c9279f9f9a3bf9ef342900590e761855a696 (diff) | |
download | dotty-e0c1d1665c8100ccad6c324e8e15e38df9b39327.tar.gz dotty-e0c1d1665c8100ccad6c324e8e15e38df9b39327.tar.bz2 dotty-e0c1d1665c8100ccad6c324e8e15e38df9b39327.zip |
Fix highlighting in search, add highlights in forwarding links
Diffstat (limited to 'docs/_layouts')
-rw-r--r-- | docs/_layouts/blog.html | 3 | ||||
-rw-r--r-- | docs/_layouts/default.html | 22 |
2 files changed, 23 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 992487de8..6fa1a1d78 100644 --- a/docs/_layouts/default.html +++ b/docs/_layouts/default.html @@ -26,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(); @@ -35,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> |