Contributions by @saivann to devel docs

Thanks also (in alphabetical order) to @cbeams, @mikehearn, and
@tgeller, among others.

The last pre-squash commit was: c2b8d562aa107c7b68c60946cea14cdccc5159ad

js/main.js

@@ -57,6 +57,42 @@ for(var i=0;i<4;i++){
 return Math.max(0,a.offsetHeight-p[0]-p[2]);
 }
 
+function getLeft(a){
+//Return the integer value of the computed distance between given node and the browser window.
+//Ex. getLeft(node);
+var b=a.offsetLeft;
+while(a.offsetParent){a=a.offsetParent;b+=a.offsetLeft;}
+return b;
+}
+
+function getTop(a){
+//Return the integer value of the computed distance between given node and the browser window.
+//Ex. getTop(node);
+var b=a.offsetTop;
+while(a.offsetParent){a=a.offsetParent;b+=a.offsetTop;}
+return b;
+}
+
+function getPageYOffset(){
+//Return the integer value for the vertical position of the scroll bar.
+return (window.pageYOffset)?window.pageYOffset:document.documentElement.scrollTop;
+}
+
+function getPageXOffset(){
+//Return the integer value for the horizontal position of the scroll bar.
+return (window.pageXOffset)?window.pageXOffset:document.documentElement.scrollLeft;
+}
+
+function getWindowY(){
+//Return the integer value for the browser window height.
+return (window.innerHeight)?window.innerHeight:document.documentElement.clientHeight;
+}
+
+function getWindowX(){
+//Return the integer value for the browser window width.
+return (window.innerWidth)?window.innerWidth:document.documentElement.clientWidth;
+}
+
 function supportsSVG(){
 //Return true if the browser supports SVG.
 //Ex. if(!supportsSVG()){..apply png fallback..}
@@ -233,6 +269,98 @@ for(var i=0,nds=document.getElementsByTagName('DIV'),n=nds.length;i<n;i++){
 removeEvent(window,'scroll',mobileWHide);
 }
 
+function updateToc(){
+//Update table of content active entry and browser url on scroll
+var pageoffset;
+var windowy;
+var toc;
+var first;
+var last;
+var closer;
+var init=function(){
+	setenv();
+	updatehistory();
+	updatetoc();
+}
+//Set variables
+var setenv=function(){
+	pageoffset=getPageYOffset();
+	windowy=getWindowY();
+	toc=document.getElementById('toc');
+	fallback=document.getElementsByTagName('H2')[0];
+	first=[fallback,getTop(fallback)];
+	last=[fallback,getTop(fallback)];
+	closer=[fallback,getTop(fallback)];
+	//Find all titles
+	var nodes=[];
+	var tags=['H2','H3','H4','H5','H6'];
+	for(var i=0,n=tags.length;i<n;i++){
+		for(var ii=0,t=document.getElementsByTagName(tags[i]),nn=t.length;ii<nn;ii++)nodes.push(t[ii]);
+	}
+	//Find first title, last title and closer title
+	for(var i=0,n=nodes.length;i<n;i++){
+		if(!nodes[i].id)continue;
+		var top=getTop(nodes[i]);
+		if(top<first[1])first=[nodes[i],top];
+		if(top>last[1])last=[nodes[i],top];
+		if(top<pageoffset+10&&top>closer[1])closer=[nodes[i],top];
+	}
+	//Set closer title to first or last title if at the top or bottom of the page
+	if(pageoffset<first[1])closer=[first[0],first[1]];
+	if(windowy+pageoffset>=getHeight(document.body))closer=[last[0],last[1]];
+}
+//Update toc position and set active toc entry
+var updatetoc=function(){
+	//Set bottom and top to fit within window and not overflow its parent node
+	var div=toc.getElementsByTagName('DIV')[0];
+	if(pageoffset>getTop(toc)){
+		div.className='scroll';
+		div.style.top='20px';
+		div.style.bottom=Math.max((pageoffset+windowy)-(getHeight(toc.parentNode)+getTop(toc.parentNode)),20)+'px';
+	}
+	else div.className='';
+	//Remove .active class from toc and find new active toc entry
+	var a=false;
+	for(var i=0,t=toc.getElementsByTagName('*'),n=t.length;i<n;i++){
+		if(t[i].className&&t[i].className.indexOf('active')!==-1)t[i].className='';
+		if(t[i].nodeName=='A'&&t[i].getAttribute('href')=='#'+closer[0].id)a=t[i];
+	}
+	if(a===false)return;
+	//Set .active class on new active toc entry
+	while(a.parentNode.nodeName=='LI'||a.parentNode.nodeName=='UL'){
+		a.className='active';
+		a=a.parentNode;
+	}
+}
+//Update browser url
+var updatehistory=function(){
+	//Don't call window.history if not supported
+	if(!window.history||!window.history.replaceState)return;
+	//Don't update window url when it doesn't need to be updated
+	if(new RegExp('#'+closer[0].id+'$').test(window.location.href.toString()))return;
+	//Don't update window url when the window is over the first title in the page
+	if(pageoffset<first[1])return;
+	//Don't update window url when page is not loaded, or user just clicked a url
+	if(!toc.hasAttribute('data-timestamp')||toc.getAttribute('data-timestamp')>new Date().getTime()-1000)return;
+	window.history.replaceState(null,null,'#'+closer[0].id);
+}
+//Update the toc when the page stops scrolling
+var evtimeout=function(){
+	toc=document.getElementById('toc');
+	clearTimeout(toc.getAttribute('data-timeout'));
+	toc.setAttribute('data-timeout',setTimeout(init,1));
+}
+//Reset timestamp on page load and each time the user clicks a url
+var evtimestamp=function(){
+	toc=document.getElementById('toc');
+	document.getElementById('toc').setAttribute('data-timestamp',new Date().getTime());
+}
+addEvent(window,'scroll',evtimeout);
+addEvent(window,'popstate',evtimestamp);
+addEvent(window,'load',evtimestamp);
+init();
+}
+
 function makeEditable(e){
 //An easter egg that makes the page editable when user click on the page and hold their mouse button for one second.
 //This trick allows translators and writers to preview their work.