merged

--- a/etc/options	Thu May 16 21:55:12 2013 +0200
+++ b/etc/options	Thu May 16 22:02: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
@@ -40,8 +24,41 @@
   -- "indentation for pretty printing of display material"
 option thy_output_source : bool = false
   -- "print original source text rather than internal representation"
+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:55:12 2013 +0200
+++ b/src/HOL/Prolog/prolog.ML	Thu May 16 22:02: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/Isar/attrib.ML	Thu May 16 21:55:12 2013 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu May 16 22:02:01 2013 +0200
@@ -57,8 +57,16 @@
     (Context.generic -> string) -> string Config.T * (theory -> theory)
   val setup_config_bool: Binding.binding -> (Context.generic -> bool) -> bool Config.T
   val setup_config_int: Binding.binding -> (Context.generic -> int) -> int Config.T
+  val setup_config_real: Binding.binding -> (Context.generic -> real) -> real Config.T
   val setup_config_string: Binding.binding -> (Context.generic -> string) -> string Config.T
-  val setup_config_real: Binding.binding -> (Context.generic -> real) -> real Config.T
+  val option_bool: string -> bool Config.T * (theory -> theory)
+  val option_int: string -> int Config.T * (theory -> theory)
+  val option_real: string -> real Config.T * (theory -> theory)
+  val option_string: string -> string Config.T * (theory -> theory)
+  val setup_option_bool: string -> bool Config.T
+  val setup_option_int: string -> int Config.T
+  val setup_option_real: string -> real Config.T
+  val setup_option_string: string -> string Config.T
 end;
 
 structure Attrib: ATTRIB =
@@ -476,19 +484,19 @@
 fun declare make coerce binding default =
   let
     val name = Binding.name_of binding;
-    val config_value = Config.declare_generic {global = false} name (make o default);
+    val config_value = Config.declare name (make o default);
     val config = coerce config_value;
   in (config, register binding config_value) end;
 
 in
 
+fun register_config config = register (Binding.name (Config.name_of config)) config;
+
 val config_bool = declare Config.Bool Config.bool;
 val config_int = declare Config.Int Config.int;
 val config_real = declare Config.Real Config.real;
 val config_string = declare Config.String Config.string;
 
-fun register_config config = register (Binding.name (Config.name_of config)) config;
-
 end;
 
 
@@ -512,6 +520,36 @@
 end;
 
 
+(* system options *)
+
+local
+
+fun declare_option coerce name =
+  let
+    val config = Config.declare_option name;
+  in (coerce config, register_config config) end;
+
+fun setup_option coerce name =
+  let
+    val config = Config.declare_option name;
+    val _ = Context.>> (Context.map_theory (register_config config));
+  in coerce config end;
+
+in
+
+val option_bool = declare_option Config.bool;
+val option_int = declare_option Config.int;
+val option_real = declare_option Config.real;
+val option_string = declare_option Config.string;
+
+val setup_option_bool = setup_option Config.bool;
+val setup_option_int = setup_option Config.int;
+val setup_option_real = setup_option Config.real;
+val setup_option_string = setup_option Config.string;
+
+end;
+
+
 (* theory setup *)
 
 val _ = Context.>> (Context.map_theory

--- a/src/Pure/Syntax/printer.ML	Thu May 16 21:55:12 2013 +0200
+++ b/src/Pure/Syntax/printer.ML	Thu May 16 22:02: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:55:12 2013 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Thu May 16 22:02: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/Thy/thy_output.ML	Thu May 16 21:55:12 2013 +0200
+++ b/src/Pure/Thy/thy_output.ML	Thu May 16 22:02:01 2013 +0200
@@ -6,16 +6,12 @@
 
 signature THY_OUTPUT =
 sig
-  val display_default: bool Unsynchronized.ref
-  val quotes_default: bool Unsynchronized.ref
-  val indent_default: int Unsynchronized.ref
-  val source_default: bool Unsynchronized.ref
-  val break_default: bool Unsynchronized.ref
   val display: bool Config.T
   val quotes: bool Config.T
   val indent: int Config.T
   val source: bool Config.T
   val break: bool Config.T
+  val modes: string Config.T
   val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
   val add_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
   val intern_command: theory -> xstring -> string
@@ -29,7 +25,6 @@
   val boolean: string -> bool
   val integer: string -> int
   datatype markup = Markup | MarkupEnv | Verbatim
-  val modes: string list Unsynchronized.ref
   val eval_antiq: Scan.lexicon -> Toplevel.state -> Symbol_Pos.T list * Position.range -> string
   val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
   val check_text: Symbol_Pos.text * Position.T -> Toplevel.state -> unit
@@ -48,19 +43,14 @@
 structure Thy_Output: THY_OUTPUT =
 struct
 
-(** global options **)
+(** options **)
 
-val display_default = Unsynchronized.ref false;
-val quotes_default = Unsynchronized.ref false;
-val indent_default = Unsynchronized.ref 0;
-val source_default = Unsynchronized.ref false;
-val break_default = Unsynchronized.ref false;
-
-val display = Attrib.setup_config_bool (Binding.name "thy_output_display") (fn _ => ! display_default);
-val quotes = Attrib.setup_config_bool (Binding.name "thy_output_quotes") (fn _ => ! quotes_default);
-val indent = Attrib.setup_config_int (Binding.name "thy_output_indent") (fn _ => ! indent_default);
-val source = Attrib.setup_config_bool (Binding.name "thy_output_source") (fn _ => ! source_default);
-val break = Attrib.setup_config_bool (Binding.name "thy_output_break") (fn _ => ! break_default);
+val display = Attrib.setup_option_bool "thy_output_display";
+val break = Attrib.setup_option_bool "thy_output_break";
+val quotes = Attrib.setup_option_bool "thy_output_quotes";
+val indent = Attrib.setup_option_int "thy_output_indent";
+val source = Attrib.setup_option_bool "thy_output_source";
+val modes = Attrib.setup_option_string "thy_output_modes";
 
 
 structure Wrappers = Proof_Data
@@ -179,8 +169,6 @@
 
 (* eval_antiquote *)
 
-val modes = Unsynchronized.ref ([]: string list);
-
 fun eval_antiq lex state (ss, (pos, _)) =
   let
     val (opts, src) = Token.read_antiq lex antiq (ss, pos);
@@ -188,7 +176,8 @@
     val preview_ctxt = fold option opts (Toplevel.presentation_context_of state);
     val print_ctxt = Context_Position.set_visible false preview_ctxt;
     val _ = cmd preview_ctxt;
-  in Print_Mode.with_modes (! modes @ Latex.modes) (fn () => cmd print_ctxt) () end;
+    val print_modes = space_explode "," (Config.get print_ctxt modes) @ Latex.modes;
+  in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
 
 fun eval_antiquote lex state (txt, pos) =
   let

--- a/src/Pure/Tools/build.ML	Thu May 16 21:55:12 2013 +0200
+++ b/src/Pure/Tools/build.ML	Thu May 16 22:02:01 2013 +0200
@@ -93,11 +93,6 @@
     |> no_document options ? Present.no_document
     |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
     |> Unsynchronized.setmp Goal.skip_proofs (Options.bool options "skip_proofs")
-    |> Unsynchronized.setmp Thy_Output.display_default (Options.bool options "thy_output_display")
-    |> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes")
-    |> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent")
-    |> Unsynchronized.setmp Thy_Output.source_default (Options.bool options "thy_output_source")
-    |> Unsynchronized.setmp Thy_Output.break_default (Options.bool options "thy_output_break")
     |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
     |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
 

--- a/src/Pure/Tools/proof_general_pure.ML	Thu May 16 21:55:12 2013 +0200
+++ b/src/Pure/Tools/proof_general_pure.ML	Thu May 16 22:02: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/config.ML	Thu May 16 21:55:12 2013 +0200
+++ b/src/Pure/config.ML	Thu May 16 22:02:01 2013 +0200
@@ -24,7 +24,6 @@
   val get_generic: Context.generic -> 'a T -> 'a
   val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
   val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
-  val declare_generic: {global: bool} -> string -> (Context.generic -> value) -> raw
   val declare_global: string -> (Context.generic -> value) -> raw
   val declare: string -> (Context.generic -> value) -> raw
   val declare_option: string -> raw
@@ -110,7 +109,7 @@
   fun merge data = Inttab.merge (K true) data;
 );
 
-fun declare_generic {global} name default =
+fun declare_generic global name default =
   let
     val id = serial ();
 
@@ -136,8 +135,8 @@
       | map_value f context = update_value f context;
   in Config {name = name, get_value = get_value, map_value = map_value} end;
 
-val declare_global = declare_generic {global = true};
-val declare = declare_generic {global = false};
+val declare_global = declare_generic true;
+val declare = declare_generic false;
 
 fun declare_option name =
   let

--- a/src/Pure/display.ML	Thu May 16 21:55:12 2013 +0200
+++ b/src/Pure/display.ML	Thu May 16 22:02: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:55:12 2013 +0200
+++ b/src/Pure/goal_display.ML	Thu May 16 22:02: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