// Functions for documentation navigation

    function setSelectorFromURL()
    {
      var o = document.selectorForm.selector.options;
      var path = location.pathname;
      for(var i = 0; i < o.length; i++)
      {
        if(o[i].value != ''
          && path.indexOf(o[i].value) == path.length - o[i].value.length)
          document.selectorForm.selector.selectedIndex = i;
      }
      path = location.href;
      for(var i = 0; i < o.length; i++)
      {
        if(o[i].value != ''
          && path.indexOf(o[i].value) == path.length - o[i].value.length)
          document.selectorForm.selector.selectedIndex = i;
      }
    }
    
    function selectorChanged()
    {
      var i = document.selectorForm.selector.selectedIndex;
      var o = document.selectorForm.selector.options[i];
      if(o.value != '')
        location.href = o.value;
    }