more system options as context-sensitive config 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)"
 

--- a/src/HOL/Prolog/prolog.ML	Thu May 16 21:09:58 2013 +0200
+++ b/src/HOL/Prolog/prolog.ML	Thu May 16 21:48:01 2013 +0200
@@ -2,7 +2,7 @@
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
 *)
 
-Goal_Display.show_main_goal_default := true;
+Options.default_put_bool @{option show_main_goal} true;
 
 structure Prolog =
 struct

--- a/src/Pure/Syntax/printer.ML	Thu May 16 21:09:58 2013 +0200
+++ b/src/Pure/Syntax/printer.ML	Thu May 16 21:48:01 2013 +0200
@@ -20,11 +20,8 @@
 signature PRINTER =
 sig
   include BASIC_PRINTER
-  val show_brackets_default: bool Unsynchronized.ref
   val show_brackets_raw: Config.raw
-  val show_types_default: bool Unsynchronized.ref
   val show_types_raw: Config.raw
-  val show_sorts_default: bool Unsynchronized.ref
   val show_sorts_raw: Config.raw
   val show_markup_default: bool Unsynchronized.ref
   val show_markup_raw: Config.raw
@@ -53,17 +50,13 @@
 
 (** options for printing **)
 
-val show_brackets_default = Unsynchronized.ref false;
-val show_brackets_raw =
-  Config.declare "show_brackets" (fn _ => Config.Bool (! show_brackets_default));
+val show_brackets_raw = Config.declare_option "show_brackets";
 val show_brackets = Config.bool show_brackets_raw;
 
-val show_types_default = Unsynchronized.ref false;
-val show_types_raw = Config.declare "show_types" (fn _ => Config.Bool (! show_types_default));
+val show_types_raw = Config.declare_option "show_types";
 val show_types = Config.bool show_types_raw;
 
-val show_sorts_default = Unsynchronized.ref false;
-val show_sorts_raw = Config.declare "show_sorts" (fn _ => Config.Bool (! show_sorts_default));
+val show_sorts_raw = Config.declare_option "show_sorts";
 val show_sorts = Config.bool show_sorts_raw;
 
 val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true));

--- a/src/Pure/Syntax/syntax_trans.ML	Thu May 16 21:09:58 2013 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Thu May 16 21:48:01 2013 +0200
@@ -28,7 +28,6 @@
   val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
-  val eta_contract_default: bool Unsynchronized.ref
   val eta_contract_raw: Config.raw
   val mark_bound_abs: string * typ -> term
   val mark_bound_body: string * typ -> term
@@ -303,8 +302,7 @@
       | t' => Abs (a, T, t'))
   | eta_abs t = t;
 
-val eta_contract_default = Unsynchronized.ref true;
-val eta_contract_raw = Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default));
+val eta_contract_raw = Config.declare_option "eta_contract";
 val eta_contract = Config.bool eta_contract_raw;
 
 fun eta_contr ctxt tm =

--- a/src/Pure/Tools/proof_general_pure.ML	Thu May 16 21:09:58 2013 +0200
+++ b/src/Pure/Tools/proof_general_pure.ML	Thu May 16 21:48:01 2013 +0200
@@ -8,23 +8,23 @@
 (* display *)
 
 val _ =
-  ProofGeneral.preference_bool ProofGeneral.category_display
+  ProofGeneral.preference_option ProofGeneral.category_display
     NONE
-    Printer.show_types_default
+    @{option show_types}
     "show-types"
     "Include types in display of Isabelle terms";
 
 val _ =
-  ProofGeneral.preference_bool ProofGeneral.category_display
+  ProofGeneral.preference_option ProofGeneral.category_display
     NONE
-    Printer.show_sorts_default
+    @{option show_sorts}
     "show-sorts"
-    "Include sorts in display of Isabelle terms";
+    "Include sorts in display of Isabelle types";
 
 val _ =
-  ProofGeneral.preference_bool ProofGeneral.category_display
+  ProofGeneral.preference_option ProofGeneral.category_display
     NONE
-    Goal_Display.show_consts_default
+    @{option show_consts}
     "show-consts"
     "Show types of consts in Isabelle goal display";
 
@@ -36,23 +36,23 @@
     "Show fully qualified names in Isabelle terms";
 
 val _ =
-  ProofGeneral.preference_bool ProofGeneral.category_display
+  ProofGeneral.preference_option ProofGeneral.category_display
     NONE
-    Printer.show_brackets_default
+    @{option show_brackets}
     "show-brackets"
     "Show full bracketing in Isabelle terms";
 
 val _ =
-  ProofGeneral.preference_bool ProofGeneral.category_display
+  ProofGeneral.preference_option ProofGeneral.category_display
     NONE
-    Goal_Display.show_main_goal_default
+    @{option show_main_goal}
     "show-main-goal"
     "Show main goal in proof state display";
 
 val _ =
-  ProofGeneral.preference_bool ProofGeneral.category_display
+  ProofGeneral.preference_option ProofGeneral.category_display
     NONE
-    Syntax_Trans.eta_contract_default
+    @{option eta_contract}
     "eta-contract"
     "Print terms eta-contracted";
 

--- a/src/Pure/display.ML	Thu May 16 21:09:58 2013 +0200
+++ b/src/Pure/display.ML	Thu May 16 21:48:01 2013 +0200
@@ -7,7 +7,6 @@
 
 signature BASIC_DISPLAY =
 sig
-  val show_consts_default: bool Unsynchronized.ref
   val show_consts: bool Config.T
   val show_hyps_raw: Config.raw
   val show_hyps: bool Config.T
@@ -34,7 +33,6 @@
 
 (** options **)
 
-val show_consts_default = Goal_Display.show_consts_default;
 val show_consts = Goal_Display.show_consts;
 
 val show_hyps_raw = Config.declare "show_hyps" (fn _ => Config.Bool false);

--- a/src/Pure/goal_display.ML	Thu May 16 21:09:58 2013 +0200
+++ b/src/Pure/goal_display.ML	Thu May 16 21:48:01 2013 +0200
@@ -9,10 +9,8 @@
 sig
   val goals_limit_raw: Config.raw
   val goals_limit: int Config.T
-  val show_main_goal_default: bool Unsynchronized.ref
   val show_main_goal_raw: Config.raw
   val show_main_goal: bool Config.T
-  val show_consts_default: bool Unsynchronized.ref
   val show_consts_raw: Config.raw
   val show_consts: bool Config.T
   val pretty_flexpair: Proof.context -> term * term -> Pretty.T
@@ -28,13 +26,10 @@
 val goals_limit_raw = Config.declare_option "goals_limit";
 val goals_limit = Config.int goals_limit_raw;
 
-val show_main_goal_default = Unsynchronized.ref false;
-val show_main_goal_raw =
-  Config.declare "show_main_goal" (fn _ => Config.Bool (! show_main_goal_default));
+val show_main_goal_raw = Config.declare_option "show_main_goal";
 val show_main_goal = Config.bool show_main_goal_raw;
 
-val show_consts_default = Unsynchronized.ref false;
-val show_consts_raw = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default));
+val show_consts_raw = Config.declare_option "show_consts";
 val show_consts = Config.bool show_consts_raw;
 
 fun pretty_flexpair ctxt (t, u) = Pretty.block