etc/options

--- a/etc/options	Thu Jul 26 17:16:02 2012 +0200
+++ b/etc/options	Thu Jul 26 17:17:53 2012 +0200
@@ -27,5 +27,11 @@
 declare names_short : bool = false
 declare names_unique : bool = true
 
+declare thy_output_display : bool = false
+declare thy_output_quotes : bool = false
+declare thy_output_indent : int = 0
+declare thy_output_source : bool = false
+declare thy_output_break : bool = false
+
 declare timing : bool = false