diff options
author | Felix Mulder <felix.mulder@gmail.com> | 2016-11-07 15:36:20 +0100 |
---|---|---|
committer | Felix Mulder <felix.mulder@gmail.com> | 2016-11-07 15:57:52 +0100 |
commit | fb0f3ff8c8e5a2e3b906dd9a8815a2d22ca9c38c (patch) | |
tree | f99953c897acd0c2fabf75060e1845650547ccac /docs/search.html | |
parent | 5d590242132b0f38fc04afed2c787dadfd8d6c2f (diff) | |
download | dotty-fb0f3ff8c8e5a2e3b906dd9a8815a2d22ca9c38c.tar.gz dotty-fb0f3ff8c8e5a2e3b906dd9a8815a2d22ca9c38c.tar.bz2 dotty-fb0f3ff8c8e5a2e3b906dd9a8815a2d22ca9c38c.zip |
Fix #1674: add search to doc site
Diffstat (limited to 'docs/search.html')
-rw-r--r-- | docs/search.html | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/docs/search.html b/docs/search.html new file mode 100644 index 000000000..acd55b798 --- /dev/null +++ b/docs/search.html @@ -0,0 +1,35 @@ +--- +layout: search +title: "Search" +--- +<h1 id="search">Search Results</h1> + +<form id="search-bar" action="/search.html" method="get"> + <input placeholder="Search" type="text" id="search-box" name="query"> +</form> + +<ul id="search-results"></ul> + +<script> + window.store = { + {% for post in site.posts %} + "{{ post.url | slugify }}": { + "title": "{{ post.title | xml_escape }}", + "author": "{{ post.author | xml_escape }}", + "content": {{ post.content | markdownify | strip_html | lstrip | jsonify }}, + "url": "{{ post.url | xml_escape }}" + }, + {% endfor %} + {% for page in site.html_pages %} + "{{ page.url | slugify }}": { + "title": "{{ page.title | xml_escape }}", + "name": "{{ page.name | xml_escape }}", + "content": {{ page.content | markdownify | strip_html | lstrip | jsonify }}, + "url": "{{ page.url | xml_escape }}" + } + {% unless forloop.last %},{% endunless %} + {% endfor %} + }; +</script> +<script src="/js/lunr.min.js"></script> +<script src="/js/search.js"></script> |