Reduced stream poll interval

src/data/document.py

@@ -8,6 +8,7 @@ from unicodedata import normalize
 from urllib.parse import quote as url_encode
 from urllib.parse import unquote as url_decode
 import string
+import json
 
 def os_path_separators():
 	seps = ['/','\\']
@@ -53,11 +54,20 @@ class Document:
 		self.doc_path = doc_path
 		self.valid = True
 		
-		# TODO: actually read document settings
+		# Init default values
 		self.settings = {
 			'multiversion': False,
-			'default_version': 'main'
+			'default_version': ''
 		}
+		
+		# Read settings.json (if it exists)
+		json_settings_filename = self.doc_path + '/settings.json'
+		if os.path.exists(json_settings_filename):
+			with open(json_settings_filename) as f:
+				json_settings = json.load(f)
+			for key in self.settings:
+				if key in json_settings:
+					self.settings[key] = json_settings[key]
 	
 	def build(self):
 		multiversion_build = self.settings['multiversion']

src/static/log-stream.js

@@ -25,7 +25,11 @@ function log_stream(element, logUrl) {
 					}
 				}
 				else {
-					setTimeout(fetchMore, 100);
+					let delay = 500;
+					if(json.new_output != '') {
+						delay = 100;
+					}
+					setTimeout(fetchMore, delay);
 				}
 			});
 	}