| 
									
										
										
										
											2018-08-29 20:44:35 +02:00
										 |  |  | /*global document */ | 
					
						
							| 
									
										
										
										
											2019-08-20 21:40:47 +02:00
										 |  |  | (() => { | 
					
						
							|  |  |  |     const source = document.getElementsByClassName('prettyprint source linenums'); | 
					
						
							|  |  |  |     let i = 0; | 
					
						
							|  |  |  |     let lineNumber = 0; | 
					
						
							|  |  |  |     let lineId; | 
					
						
							|  |  |  |     let lines; | 
					
						
							|  |  |  |     let totalLines; | 
					
						
							|  |  |  |     let anchorHash; | 
					
						
							| 
									
										
										
										
											2018-08-29 20:44:35 +02:00
										 |  |  | 
 | 
					
						
							|  |  |  |     if (source && source[0]) { | 
					
						
							|  |  |  |         anchorHash = document.location.hash.substring(1); | 
					
						
							|  |  |  |         lines = source[0].getElementsByTagName('li'); | 
					
						
							|  |  |  |         totalLines = lines.length; | 
					
						
							|  |  |  | 
 | 
					
						
							|  |  |  |         for (; i < totalLines; i++) { | 
					
						
							|  |  |  |             lineNumber++; | 
					
						
							| 
									
										
										
										
											2019-08-20 21:40:47 +02:00
										 |  |  |             lineId = `line${lineNumber}`; | 
					
						
							| 
									
										
										
										
											2018-08-29 20:44:35 +02:00
										 |  |  |             lines[i].id = lineId; | 
					
						
							|  |  |  |             if (lineId === anchorHash) { | 
					
						
							|  |  |  |                 lines[i].className += ' selected'; | 
					
						
							|  |  |  |             } | 
					
						
							|  |  |  |         } | 
					
						
							|  |  |  |     } | 
					
						
							|  |  |  | })(); |