--- a/etc/options Tue Sep 11 16:10:54 2012 +0200
+++ b/etc/options Tue Sep 11 19:19:39 2012 +0200
@@ -80,3 +80,18 @@
option timeout : real = 0
-- "timeout for session build job (seconds > 0)"
+
+section {* Editor session parameters *}
+
+option editor_load_delay : real = 0.5
+ -- "delay for file load operations (new buffers etc.)"
+
+option editor_input_delay : real = 0.3
+ -- "delay for user input (text edits, cursor movement etc.)"
+
+option editor_output_delay : real = 0.1
+ -- "delay for prover output (markup, common messages etc.)"
+
+option editor_update_delay : real = 0.5
+ -- "delay for physical GUI updates"
+