etc/options
changeset 69103 814a1ab42d70
parent 68661 5820f0f379ae
child 69353 a6e83dcc00e6
equal deleted inserted replaced
69102:4b06a20b13b5 69103:814a1ab42d70
   172 
   172 
   173 public option editor_reparse_limit : int = 10000
   173 public option editor_reparse_limit : int = 10000
   174   -- "maximum amount of reparsed text outside perspective"
   174   -- "maximum amount of reparsed text outside perspective"
   175 
   175 
   176 public option editor_tracing_messages : int = 1000
   176 public option editor_tracing_messages : int = 1000
   177   -- "initial number of tracing messages for each command transaction"
   177   -- "initial number of tracing messages for each command transaction (0: unbounded)"
   178 
   178 
   179 public option editor_chart_delay : real = 3.0
   179 public option editor_chart_delay : real = 3.0
   180   -- "delay for chart repainting"
   180   -- "delay for chart repainting"
   181 
   181 
   182 public option editor_continuous_checking : bool = true
   182 public option editor_continuous_checking : bool = true