add doc version switcher to top of sidebar

doc/.static/fix_rtd.css

@@ -2,3 +2,10 @@
 .rst-content table.field-list .field-body {
     padding-top: 8px;
 }
+.rst-versions-up {
+    cursor: pointer;
+    display: inline;
+}
+.wy-side-nav-search>div.version {
+    color: white;
+}

doc/.static/version_switch.js

@@ -68,10 +68,27 @@
     return vswitch.join('');
   }
 
+  function build_vswitch_up() {
+  // Build HTML string for version selector, based on ReadTheDocs theme's versions.html
+
+    var vlabel = current_version.replace("theano_versions/", "");
+    if (vlabel == 'theano') {
+      vlabel = 'release';
+    }
+    var vswitch = ['<div class="rst-versions-up" data-toggle="rst-versions" role="note" aria-label="versions" align=center>'];
+    vswitch.push('<span class="rst-current-version" data-toggle="rst-current-version">');
+    vswitch.push(vlabel);
+    vswitch.push('<span class="fa fa-caret-down"></span>');
+    vswitch.push('</span>');
+    vswitch.push('</div>');
+    return vswitch.join('');
+  }
+
 // Create HTML for version switcher and assign to placeholder in layout.html.
   $(document).ready(function() {
     // Build default switcher
     $('.version_switcher_placeholder').html(build_vswitch());
+    $('.version_switcher_placeholder_up').html(build_vswitch_up());
 
     // Check server for other doc versions and update switcher.
     if (url.startsWith('http')) {
@@ -79,7 +96,8 @@
         $.each(data, function(version, dir) {
             versions_dir[version] = dir;
         });
-        $('.version_switcher_placeholder').html(build_vswitch()); 
+        $('.version_switcher_placeholder').html(build_vswitch());
+        $('.version_switcher_placeholder_up').html(build_vswitch_up());
       });
     }    
   });

doc/.templates/layout.html

@@ -14,7 +14,7 @@
   })();
 </script>
 
-<!--Insert version switcher at bottom of sidebar-->
+<!--Insert version switcher at bottom and top of sidebar-->
 <script type="text/javascript">
   var span = document.createElement("SPAN")
   var span_class = document.createAttribute("class");
@@ -24,6 +24,13 @@
   div.appendChild(span);
   var nav_div = document.getElementsByClassName("wy-nav-side")[0];
   nav_div.appendChild(div);
+
+  var span_up = document.createElement("SPAN")
+  var span_class_up = document.createAttribute("class");
+  span_class_up.value = "version_switcher_placeholder_up";
+  span_up.setAttributeNode(span_class_up);
+  var nav_div_up = document.getElementsByClassName("version")[0];
+  nav_div_up.appendChild(span_up);
 </script>
 
 <script type="text/javascript"