blitz
/
monkey2
mirror of https://github.com/blitz-research/monkey2.git


			
				
					
						
						
							123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105
							<!doctype html>

<html>

<head>

	<meta charset="utf-8">

	<title>Monkey2 Language Reference</title>

	<link rel="stylesheet" href="style.css">
	
	<link rel="stylesheet" href="jstree/dist/themes/default/style.min.css" />

	<script src="jstree/dist/libs/jquery-1.9.1.min.js"></script>

	<script src="jstree/dist/jstree.min.js"></script>

	<script>

	window.onload=function(){

		document.getElementById( 'docs' ).src="The Monkey2 Language.html";
	}

	function scrollToTopic( id ){
 
		var childWindow=document.getElementById( 'docs' ).contentWindow;

		childWindow.scrollTo( 0,childWindow.document.getElementById( id ).offsetTop-16 );
	}

	</script>

</head>

<body class="page_body">

<div class="modules_content">

<!-- CONTENT -->

<div class="modules_nav_wrapper">
<form role="search"><input type="text" id="search" placeholder="Topic search" style="width:100%;" /></form>
<div id="tree" class="modules_nav_tree"></div>
</div>

<div class="modules_docs_wrapper">
<iframe id="docs" class="modules_docs_iframe"></iframe>
</div>

<script>

jQuery( function($){

	$('#tree').jstree( {

		'core':{
			'multiple' : false,
			'animation' : false,
			'themes':{
				'dots' : false,
				'icons' : false,
				'stripes' : false
			},
			'data':[ ${LANG_NAV} ]
		},
		'plugins':[ 'search' ]
 	});
 	
	$('#tree').on( 'changed.jstree',function( e,data ){

		var node=data.instance.get_node( data.selected[0] );
		if( !node || !node.data ) return;

		var topic=node.data.topic;
		if( !topic ) return;

		scrollToTopic( topic );
	} );
	
	var to=false;

	$('#search').keyup( function(){

		if( to ) { clearTimeout( to ); }

		to = setTimeout( function(){
			var v = $('#search').val();
			$('#tree').jstree( true ).search( v );
		},250 );

	});

} );	
	
</script>

<!-- END -->

</div>

</body>

</html>