etc/options
changeset 49288 2c9272cb4568
parent 49270 e5d162d15867
child 49290 64bed36cd8da
     1.1 --- a/etc/options	Tue Sep 11 16:10:54 2012 +0200
     1.2 +++ b/etc/options	Tue Sep 11 19:19:39 2012 +0200
     1.3 @@ -80,3 +80,18 @@
     1.4  option timeout : real = 0
     1.5    -- "timeout for session build job (seconds > 0)"
     1.6  
     1.7 +
     1.8 +section {* Editor session parameters *}
     1.9 +
    1.10 +option editor_load_delay : real = 0.5
    1.11 +  -- "delay for file load operations (new buffers etc.)"
    1.12 +
    1.13 +option editor_input_delay : real = 0.3
    1.14 +  -- "delay for user input (text edits, cursor movement etc.)"
    1.15 +
    1.16 +option editor_output_delay : real = 0.1
    1.17 +  -- "delay for prover output (markup, common messages etc.)"
    1.18 +
    1.19 +option editor_update_delay : real = 0.5
    1.20 +  -- "delay for physical GUI updates"
    1.21 +