Change html build to make versioned documentation with a dropdown menu

This changes the documentation theme to use the readthedocs theme, with
some JavaScript that provides capabilities for a dropdown menu allowing
you to select between different versions.

This mimics the changes in ESMCI/cime#3439,
which in turn was based on ESCOMP/CISM-wrapper#23.

doc/source/_static/pop_ver.js

@@ -0,0 +1,37 @@
+$(document).ready(function() {
+    /* For a URL that looks like
+    https://blah.github.io/versions/VERSIONFOO/html/bar/index.html, set cur_version_dir to
+    'VERSIONFOO' (i.e., the portion of the path following 'versions').
+    */
+    var proj_end = document.baseURI.indexOf("versions") + 9;
+    var end = document.baseURI.indexOf("/", proj_end);
+    var cur_version_dir = document.baseURI.substring(proj_end, end);
+    var mylist = $("#version-list");
+    mylist.empty();
+    $.getJSON(version_json_loc, function(data) {
+        if (data.hasOwnProperty(cur_version_dir)) {
+            /* First add the current version so that it appears first in the drop-down
+               menu and starts as the selected element of the menu. If you click on the
+               current version, you should stay at the current page.
+
+               The conditional around this block should generally be true, but we check it
+               just in case the current version is missing from the versions.json file for
+               some reason.
+            */
+            cur_version_name = data[cur_version_dir];
+            mylist.append($("<option>", {value: document.baseURI, text: cur_version_name}));
+        }
+        // Now add the other versions
+        $.each(data, function(version_dir, version_name) {
+            if (version_dir != cur_version_dir) {
+                /* If you click on a different version, you should go to the root of the
+                   documentation for that version. This assumes paths like
+                   https://blah.github.io/versions/VERSIONFOO/html/bar/index.html. So we
+                   need to go up two levels from the URL_ROOT (html) to then go back down
+                   into the appropriate version's html directory.
+                */
+                mylist.append($("<option>", {value: DOCUMENTATION_OPTIONS.URL_ROOT + '../../' + version_dir + '/html', text: version_name}));
+            }
+        });
+    });
+});

doc/source/_templates/footer.html

@@ -0,0 +1,5 @@
+{% extends "!footer.html" %}
+{% block extrafooter %}
+    {{ super() }}
+<script>var version_json_loc = "{{ pathto('../../versions.json', 1) }}";</script>
+{% endblock %}

doc/source/_templates/layout.html

@@ -0,0 +1,3 @@
+{% extends "!layout.html" %}
+
+{% set script_files = script_files + ["_static/pop_ver.js"] %}

doc/source/conf.py

@@ -16,8 +16,11 @@
 # add these directories to sys.path here. If the directory is relative to the
 # documentation root, use os.path.abspath to make it absolute, like shown here.
 #
-# import os
-# import sys
+import os
+import sys
+# Note that we need a specific version of sphinx_rtd_theme. This can be obtained with:
+# pip install git+https://github.com/esmci/sphinx_rtd_theme.git@version-dropdown-with-fixes
+import sphinx_rtd_theme
 # sys.path.insert(0, os.path.abspath('.'))
 
 
@@ -88,13 +91,20 @@
 # The theme to use for HTML and HTML Help pages.  See the documentation for
 # a list of builtin themes.
 #
-html_theme = 'bizstyle'
+html_theme = 'sphinx_rtd_theme'
 
 # Theme options are theme-specific and customize the look and feel of a theme
 # further.  For a list of options available for each theme, see the
 # documentation.
 #
-# html_theme_options = {}
+# The 'versions' option needs to have at least two versions to work, but it doesn't need
+# to have all versions: others will be added dynamically. Note that this maps from version
+# names to html links. The current version can link to the current location (i.e., do
+# nothing). For the other version, we just add a place-holder; its name and value are
+# unimportant because these versions will get replaced dynamically.
+html_theme_options = {}
+html_theme_options['versions'] = {version: ''}
+html_theme_options['versions']['[placeholder]'] = ''
 
 # Add any paths that contain custom static files (such as style sheets) here,
 # relative to this directory. They are copied after the builtin static files,