diff -r aae07a3ff536 -r 286629271d65 etc/options
--- a/etc/options	Thu May 16 21:09:58 2013 +0200
+++ b/etc/options	Thu May 16 21:48:01 2013 +0200
@@ -14,22 +14,6 @@
 option document_graph : bool = false
   -- "generate session graph image for document"
 
-option goals_limit : int = 10
-  -- "maximum number of subgoals to be printed"
-
-option show_question_marks : bool = true
-  -- "show leading question mark of schematic variables"
-
-option names_long : bool = false
-  -- "show fully qualified names"
-option names_short : bool = false
-  -- "show base names only"
-option names_unique : bool = true
-  -- "show partially qualified names, as required for unique name resolution"
-
-option pretty_margin : int = 76
-  -- "right margin / page width of pretty printer in Isabelle/ML"
-
 option thy_output_display : bool = false
   -- "indicate output as multi-line display-style material"
 option thy_output_break : bool = false
@@ -43,6 +27,38 @@
 option thy_output_modes : string = ""
   -- "additional print modes for document output (separated by commas)"
 
+
+section "Prover Output"
+
+option show_types : bool = false
+  -- "show type constraints when printing terms"
+option show_sorts : bool = false
+  -- "show sort constraints when printing types"
+option show_brackets : bool = false
+  -- "show extra brackets when printing terms/types"
+option show_question_marks : bool = true
+  -- "show leading question mark of schematic variables"
+
+option show_consts : bool = false
+  -- "show constants with types when printing proof state"
+option show_main_goal : bool = false
+  -- "show main goal when printing proof state"
+option goals_limit : int = 10
+  -- "maximum number of subgoals to be printed"
+
+option names_long : bool = false
+  -- "show fully qualified names"
+option names_short : bool = false
+  -- "show base names only"
+option names_unique : bool = true
+  -- "show partially qualified names, as required for unique name resolution"
+
+option eta_contract : bool = true
+  -- "print terms in eta-contracted form"
+
+option pretty_margin : int = 76
+  -- "right margin / page width of pretty printer in Isabelle/ML"
+
 option print_mode : string = ""
   -- "additional print modes for prover output (separated by commas)"