1 var cookie_namespace = 
'doxygen'; 
     2 var sidenav,navtree,content,header;
     4 function readCookie(cookie) 
     6   var myCookie = cookie_namespace+
"_"+cookie+
"=";
     9     var index = document.cookie.indexOf(myCookie);
    12       var valStart = index + myCookie.length;
    13       var valEnd = document.cookie.indexOf(
";", valStart);
    16         valEnd = document.cookie.length;
    18       var val = document.cookie.substring(valStart, valEnd);
    25 function writeCookie(cookie, val, expiration) 
    27   if (val==undefined) 
return;
    28   if (expiration == null) 
    30     var date = 
new Date();
    31     date.setTime(date.getTime()+(10*365*24*60*60*1000)); 
    32     expiration = date.toGMTString();
    34   document.cookie = cookie_namespace + 
"_" + cookie + 
"=" + val + 
"; expires=" + expiration+
"; path=/";
    37 function resizeWidth() 
    39   var windowWidth = $(window).width() + 
"px";
    40   var sidenavWidth = $(sidenav).outerWidth();
    41   content.css({marginLeft:parseInt(sidenavWidth)+
"px"}); 
    42   writeCookie(
'width',sidenavWidth, null);
    45 function restoreWidth(navWidth)
    47   var windowWidth = $(window).width() + 
"px";
    48   content.css({marginLeft:parseInt(navWidth)+6+
"px"});
    49   sidenav.css({width:navWidth + 
"px"});
    52 function resizeHeight() 
    54   var headerHeight = header.outerHeight();
    55   var footerHeight = footer.outerHeight();
    56   var windowHeight = $(window).height() - headerHeight - footerHeight;
    57   content.css({height:windowHeight + 
"px"});
    58   navtree.css({height:windowHeight + 
"px"});
    59   sidenav.css({height:windowHeight + 
"px"});
    62 function initResizable()
    65   sidenav = $(
"#side-nav");
    66   content = $(
"#doc-content");
    67   navtree = $(
"#nav-tree");
    68   footer  = $(
"#nav-path");
    69   $(
".side-nav-resizable").resizable({resize: 
function(e, ui) { resizeWidth(); } });
    70   $(window).resize(
function() { resizeHeight(); });
    71   var width = readCookie(
'width');
    72   if (width) { restoreWidth(width); } 
else { resizeWidth(); }
    74   var url = location.href;
    75   var i=url.indexOf(
"#");
    76   if (i>=0) window.location.hash=url.substr(i);
    77   var _preventDefault = 
function(evt) { evt.preventDefault(); };
    78   $(
"#splitbar").bind(
"dragstart", _preventDefault).bind(
"selectstart", _preventDefault);
    79   $(document).bind(
'touchmove',
function(e){
    80     var device = navigator.userAgent.toLowerCase();
    81     var ios = device.match(/(iphone|ipod|ipad)/);
    84         var target = e.target;
    86           if ($(target).css(
'-webkit-overflow-scrolling')==
'touch') 
return;
    87           target = target.parentNode;