some system options as context-sensitive config options;
authorwenzelm
Thu May 16 20:50:01 2013 +0200 (2013-05-16 ago)
changeset 5204180e001b85332
parent 52040 852939d19216
child 52042 aae07a3ff536
some system options as context-sensitive config options;
src/Pure/Thy/thy_output.ML
src/Pure/Tools/build.ML
     1.1 --- a/src/Pure/Thy/thy_output.ML	Thu May 16 20:33:01 2013 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Thu May 16 20:50:01 2013 +0200
     1.3 @@ -6,11 +6,6 @@
     1.4  
     1.5  signature THY_OUTPUT =
     1.6  sig
     1.7 -  val display_default: bool Unsynchronized.ref
     1.8 -  val quotes_default: bool Unsynchronized.ref
     1.9 -  val indent_default: int Unsynchronized.ref
    1.10 -  val source_default: bool Unsynchronized.ref
    1.11 -  val break_default: bool Unsynchronized.ref
    1.12    val display: bool Config.T
    1.13    val quotes: bool Config.T
    1.14    val indent: int Config.T
    1.15 @@ -50,17 +45,11 @@
    1.16  
    1.17  (** global options **)
    1.18  
    1.19 -val display_default = Unsynchronized.ref false;
    1.20 -val quotes_default = Unsynchronized.ref false;
    1.21 -val indent_default = Unsynchronized.ref 0;
    1.22 -val source_default = Unsynchronized.ref false;
    1.23 -val break_default = Unsynchronized.ref false;
    1.24 -
    1.25 -val display = Attrib.setup_config_bool (Binding.name "thy_output_display") (fn _ => ! display_default);
    1.26 -val quotes = Attrib.setup_config_bool (Binding.name "thy_output_quotes") (fn _ => ! quotes_default);
    1.27 -val indent = Attrib.setup_config_int (Binding.name "thy_output_indent") (fn _ => ! indent_default);
    1.28 -val source = Attrib.setup_config_bool (Binding.name "thy_output_source") (fn _ => ! source_default);
    1.29 -val break = Attrib.setup_config_bool (Binding.name "thy_output_break") (fn _ => ! break_default);
    1.30 +val display = Attrib.setup_option_bool "thy_output_display";
    1.31 +val break = Attrib.setup_option_bool "thy_output_break";
    1.32 +val quotes = Attrib.setup_option_bool "thy_output_quotes";
    1.33 +val indent = Attrib.setup_option_int "thy_output_indent";
    1.34 +val source = Attrib.setup_option_bool "thy_output_source";
    1.35  
    1.36  
    1.37  structure Wrappers = Proof_Data
     2.1 --- a/src/Pure/Tools/build.ML	Thu May 16 20:33:01 2013 +0200
     2.2 +++ b/src/Pure/Tools/build.ML	Thu May 16 20:50:01 2013 +0200
     2.3 @@ -93,11 +93,6 @@
     2.4      |> no_document options ? Present.no_document
     2.5      |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
     2.6      |> Unsynchronized.setmp Goal.skip_proofs (Options.bool options "skip_proofs")
     2.7 -    |> Unsynchronized.setmp Thy_Output.display_default (Options.bool options "thy_output_display")
     2.8 -    |> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes")
     2.9 -    |> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent")
    2.10 -    |> Unsynchronized.setmp Thy_Output.source_default (Options.bool options "thy_output_source")
    2.11 -    |> Unsynchronized.setmp Thy_Output.break_default (Options.bool options "thy_output_break")
    2.12      |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
    2.13      |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
    2.14