Add opensearch support

print_docs.py

@@ -655,6 +655,9 @@ def write_html_files(partition, loc_map, notes, mod_docs, instances, tactic_docs
   current_project = None
   current_filename = None
 
+  with open_outfile('opensearch.xml') as out:
+    out.write(env.get_template('opensearch.xml.j2').render())
+
 def write_site_map(partition):
   with open_outfile('sitemap.txt') as out:
     for filename in partition:

templates/base.j2

@@ -5,6 +5,7 @@
     <link rel="stylesheet" href="{{ site_root }}pygments.css">
     <link rel="stylesheet" href="{{ site_root }}pygments-dark.css">
     <link rel="shortcut icon" href="{{ site_root }}favicon.ico">
+    <link rel="search" type="application/opensearchdescription+xml" title="mathlib docs" href="{{ site_root }}opensearch.xml">
     <title>{% block title %}{% endblock %} - mathlib docs</title>
     <meta charset="UTF-8">
     <meta name="viewport" content="width=device-width, initial-scale=1">

templates/opensearch.xml.j2

@@ -0,0 +1,8 @@
+<?xml version="1.0" encoding="UTF-8" ?>
+<OpenSearchDescription xmlns="http://a9.com/-/spec/opensearch/1.1/" xmlns:moz="http://www.mozilla.org/2006/browser/search/">
+  <ShortName>mathlib</ShortName>
+  <Description>Search mathlib docs</Description>
+  <InputEncoding>UTF-8</InputEncoding>
+  <Image width="16" height="16" type="image/x-icon">{{ site_root }}/static/favicon.ico</Image>
+  <Url type="text/html" method="GET" template="{{ site_root }}/find/{searchTerms}" />
+</OpenSearchDescription>