| 
						
						
							
								
							
						
						
					 | 
					@ -4,10 +4,10 @@ def get_datetime_string | 
				
			
			
		
	
		
		
			
				
					 | 
					 | 
						let time = obj[4].split(":").join("-") | 
					 | 
					 | 
						let time = obj[4].split(":").join("-") | 
				
			
			
		
	
		
		
			
				
					 | 
					 | 
						"{date}_{time}" | 
					 | 
					 | 
						"{date}_{time}" | 
				
			
			
		
	
		
		
			
				
					 | 
					 | 
					
 | 
					 | 
					 | 
					
 | 
				
			
			
		
	
		
		
			
				
					
					 | 
					 | 
					export default def download_json_file data | 
					 | 
					 | 
					export default def download_json_file data, prefix="" | 
				
			
			
				
				
			
		
	
		
		
	
		
		
			
				
					 | 
					 | 
						let element = document.createElement 'a' | 
					 | 
					 | 
						let element = document.createElement 'a' | 
				
			
			
		
	
		
		
			
				
					 | 
					 | 
						element.setAttribute 'href', 'data:text/plain;charset=utf-8,' + window.encodeURIComponent(data) | 
					 | 
					 | 
						element.setAttribute 'href', 'data:text/plain;charset=utf-8,' + window.encodeURIComponent(data) | 
				
			
			
		
	
		
		
			
				
					
					 | 
					 | 
						element.setAttribute 'download', "{get_datetime_string!}.json" | 
					 | 
					 | 
						element.setAttribute 'download', "{prefix}{get_datetime_string!}.json" | 
				
			
			
				
				
			
		
	
		
		
	
		
		
			
				
					 | 
					 | 
						element.style.display = 'none' | 
					 | 
					 | 
						element.style.display = 'none' | 
				
			
			
		
	
		
		
			
				
					 | 
					 | 
						document.body.appendChild element | 
					 | 
					 | 
						document.body.appendChild element | 
				
			
			
		
	
		
		
			
				
					 | 
					 | 
						element.click! | 
					 | 
					 | 
						element.click! | 
				
			
			
		
	
	
		
		
			
				
					| 
						
							
								
							
						
						
						
					 | 
					
  |