etc/options
changeset 52807 b859a180936b
parent 52798 9d3c9862d1dd
child 52810 cd28423ba19f
     1.1 --- a/etc/options	Tue Jul 30 23:17:26 2013 +0200
     1.2 +++ b/etc/options	Wed Jul 31 10:54:37 2013 +0200
     1.3 @@ -123,15 +123,15 @@
     1.4  public option editor_chart_delay : real = 3.0
     1.5    -- "delay for chart repainting"
     1.6  
     1.7 +public option editor_continuous_checking : bool = true
     1.8 +  -- "continuous checking of proof document (visible and required parts)"
     1.9 +
    1.10  option editor_execution_delay : real = 0.02
    1.11    -- "delay for start of execution process after document update (seconds)"
    1.12  
    1.13  option editor_execution_priority : int = -1
    1.14    -- "execution priority of main document structure (e.g. 0, -1, -2)"
    1.15  
    1.16 -option editor_execution_range : string = "visible"
    1.17 -  -- "execution range of continuous document processing: all, none, visible"
    1.18 -
    1.19  
    1.20  section "Miscellaneous Tools"
    1.21