--- 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)"