# HG changeset patch
# User wenzelm
# Date 1368730201 -7200
# Node ID 80e001b85332fc6526329787b4333145f461c21d
# Parent  852939d192168e49b9aa895f2082414a8dfad92f
some system options as context-sensitive config options;

diff -r 852939d19216 -r 80e001b85332 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu May 16 20:33:01 2013 +0200
+++ b/src/Pure/Thy/thy_output.ML	Thu May 16 20:50:01 2013 +0200
@@ -6,11 +6,6 @@
 
 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
@@ -50,17 +45,11 @@
 
 (** global 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";
 
 
 structure Wrappers = Proof_Data
diff -r 852939d19216 -r 80e001b85332 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Thu May 16 20:33:01 2013 +0200
+++ b/src/Pure/Tools/build.ML	Thu May 16 20:50: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");