Merge doc and change searches.

This CL puts a dropdown in the SearchPanel, to choose from changes
search (default) or documentation search.

I mostly copied the css for the search button to the dropdown, with
some minor changes.

If docs are not available (e.g. built without docs), the whole dropdown
will be gone and it should be the same as before.

Screenshot: https://i.imgur.com/Qyg2VZg.png

Change-Id: I04e15327f43fc9c8002cba364b44d77f52075234

gerrit-common/src/main/java/com/google/gerrit/common/PageLinks.java

@@ -49,6 +49,7 @@ public class PageLinks {
   public static final String ADMIN_CREATE_PROJECT = "/admin/create-project/";
   public static final String ADMIN_PLUGINS = "/admin/plugins/";
   public static final String MY_GROUPS = "/groups/self";
+  public static final String DOCUMENTATION = "/Documentation/";
 
   public static String toChange(final ChangeInfo c) {
     return toChange(c.getId());
@@ -140,6 +141,10 @@ public class PageLinks {
     return SETTINGS_EXTENSION + pluginName + "/" + path;
   }
 
+  public static String toDocumentationQuery(String query) {
+    return DOCUMENTATION + KeyUtil.encode(query);
+  }
+
   private static String status(Status status) {
     switch (status) {
       case ABANDONED: