some system options as context-sensitive config options;

--- a/src/Pure/General/name_space.ML	Sun May 12 19:56:30 2013 +0200
+++ b/src/Pure/General/name_space.ML	Sun May 12 20:25:45 2013 +0200
@@ -21,13 +21,10 @@
   val markup: T -> string -> Markup.T
   val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
-  val names_long_default: bool Unsynchronized.ref
   val names_long_raw: Config.raw
   val names_long: bool Config.T
-  val names_short_default: bool Unsynchronized.ref
   val names_short_raw: Config.raw
   val names_short: bool Config.T
-  val names_unique_default: bool Unsynchronized.ref
   val names_unique_raw: Config.raw
   val names_unique: bool Config.T
   val extern: Proof.context -> T -> string -> xstring
@@ -166,16 +163,13 @@
 fun intern space xname = #1 (lookup space xname);
 
 
-val names_long_default = Unsynchronized.ref false;
-val names_long_raw = Config.declare "names_long" (fn _ => Config.Bool (! names_long_default));
+val names_long_raw = Config.declare_option "names_long";
 val names_long = Config.bool names_long_raw;
 
-val names_short_default = Unsynchronized.ref false;
-val names_short_raw = Config.declare "names_short" (fn _ => Config.Bool (! names_short_default));
+val names_short_raw = Config.declare_option "names_short";
 val names_short = Config.bool names_short_raw;
 
-val names_unique_default = Unsynchronized.ref true;
-val names_unique_raw = Config.declare "names_unique" (fn _ => Config.Bool (! names_unique_default));
+val names_unique_raw = Config.declare_option "names_unique";
 val names_unique = Config.bool names_unique_raw;
 
 fun extern ctxt space name =

--- a/src/Pure/ProofGeneral/preferences.ML	Sun May 12 19:56:30 2013 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Sun May 12 20:25:45 2013 +0200
@@ -145,7 +145,7 @@
   bool_pref Goal_Display.show_consts_default
     "show-consts"
     "Show types of consts in Isabelle goal display",
-  bool_pref Name_Space.names_long_default
+  options_pref "names_long"
     "long-names"
     "Show fully qualified names in Isabelle terms",
   bool_pref Printer.show_brackets_default
@@ -163,7 +163,7 @@
     "goals-limit"
     "Setting for maximum number of goals printed",
   print_depth_pref,
-  bool_pref Printer.show_question_marks_default
+  options_pref "show_question_marks"
     "show-question-marks"
     "Show leading question mark of variable name"];
 

--- a/src/Pure/Syntax/printer.ML	Sun May 12 19:56:30 2013 +0200
+++ b/src/Pure/Syntax/printer.ML	Sun May 12 20:25:45 2013 +0200
@@ -29,7 +29,6 @@
   val show_markup_default: bool Unsynchronized.ref
   val show_markup_raw: Config.raw
   val show_structs_raw: Config.raw
-  val show_question_marks_default: bool Unsynchronized.ref
   val show_question_marks_raw: Config.raw
   val show_type_constraint: Proof.context -> bool
   val show_sort_constraint: Proof.context -> bool
@@ -77,9 +76,7 @@
 val show_structs_raw = Config.declare "show_structs" (fn _ => Config.Bool false);
 val show_structs = Config.bool show_structs_raw;
 
-val show_question_marks_default = Unsynchronized.ref true;
-val show_question_marks_raw =
-  Config.declare "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
+val show_question_marks_raw = Config.declare_option "show_question_marks";
 val show_question_marks = Config.bool show_question_marks_raw;
 
 fun show_type_constraint ctxt = Config.get ctxt show_types orelse Config.get ctxt show_markup;

--- a/src/Pure/Tools/build.ML	Sun May 12 19:56:30 2013 +0200
+++ b/src/Pure/Tools/build.ML	Sun May 12 20:25:45 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 Printer.show_question_marks_default
-        (Options.bool options "show_question_marks")
-    |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")
-    |> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short")
-    |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique")
     |> 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")

--- a/src/Tools/WWW_Find/Start_WWW_Find.thy	Sun May 12 19:56:30 2013 +0200
+++ b/src/Tools/WWW_Find/Start_WWW_Find.thy	Sun May 12 20:25:45 2013 +0200
@@ -5,6 +5,7 @@
 theory Start_WWW_Find imports WWW_Find begin
 
 ML {*
+  Options.default_put_bool "show_question_marks" false;
   YXML_Find_Theorems.init ();
   val port = OS.Process.getEnv "SCGIPORT" |> the |> Int.fromString |> the;
   ScgiServer.server' 10 "/" port;

--- a/src/Tools/WWW_Find/find_theorems.ML	Sun May 12 19:56:30 2013 +0200
+++ b/src/Tools/WWW_Find/find_theorems.ML	Sun May 12 20:25:45 2013 +0200
@@ -55,7 +55,6 @@
   end;
 in
 
-val () = Printer.show_question_marks_default := false;
 val () = ScgiServer.register ("find_theorems", SOME Mime.html, ScgiServer.simple_handler find_theorems);
 
 end;