Add input field for search

Author: felixmulder

doc-tool/resources/_includes/sidebar.html

@@ -11,6 +11,17 @@
     <li class="index-title">
         <span>API</span>
     </li>
+    <li>
+      <input id="search-api-input" type="text" placeholder="Search API"/>
+      <script>
+          var input = document.getElementById("search-api-input");
+          input.onkeydown = function(evt) {
+              evt = evt || window.event;
+              if (evt.keyCode == 13)
+                  window.location = "{{ site.baseurl }}/api/search.html?searchTerm=" + input.value;
+          };
+      </script>
+    </li>
     {% endif %}
     {% for pkg in docs %}
         <li class="index-entity entity-package">

doc-tool/resources/css/sidebar.css

@@ -25,6 +25,14 @@ ul.index-entities {
     padding-left: 0;
 }
 
+ul.index-entities > li > input#search-api-input {
+    border: 0;
+    margin-left: 22px;
+    outline: none;
+    line-height: 35px;
+    box-shadow: inset 0 0px 0 white, inset 0 -0.5px 0 rgba(0, 0, 0, 0.5);
+}
+
 ul.toc {
     list-style-type: none;
     padding-top: 18px;

project/Build.scala

@@ -891,7 +891,7 @@ object DottyInjectedPlugin extends AutoPlugin {
      publishArtifact in Test := false,
      homepage := Some(url(dottyGithubUrl)),
      licenses += ("BSD New",
-       url("$dottyGithubUrl/blob/master/LICENSE.md")),
+       url(s"$dottyGithubUrl/blob/master/LICENSE.md")),
      scmInfo := Some(
        ScmInfo(
          url(dottyGithubUrl),