diff -r 1165f78c16d8 -r a20631db9c8a etc/options
--- a/etc/options	Sun Jul 28 20:51:15 2013 +0200
+++ b/etc/options	Mon Jul 29 12:50:16 2013 +0200
@@ -126,6 +126,9 @@
 public option editor_execution_priority : int = -2
   -- "execution priority of main document structure (e.g. 0, -1, -2)"
 
+option editor_execution_range : string = "visible"
+  -- "range of continuous document processing: all, none, visible"
+
 
 section "Miscellaneous Tools"