some system options as context-sensitive config options;
authorwenzelm
Sun May 12 20:25:45 2013 +0200 (2013-05-12 ago)
changeset 51949f6858bb224c9
parent 51948 cb5dbc9a06f9
child 51950 13fb5e4f2893
some system options as context-sensitive config options;
src/Pure/General/name_space.ML
src/Pure/ProofGeneral/preferences.ML
src/Pure/Syntax/printer.ML
src/Pure/Tools/build.ML
src/Tools/WWW_Find/Start_WWW_Find.thy
src/Tools/WWW_Find/find_theorems.ML
     1.1 --- a/src/Pure/General/name_space.ML	Sun May 12 19:56:30 2013 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Sun May 12 20:25:45 2013 +0200
     1.3 @@ -21,13 +21,10 @@
     1.4    val markup: T -> string -> Markup.T
     1.5    val is_concealed: T -> string -> bool
     1.6    val intern: T -> xstring -> string
     1.7 -  val names_long_default: bool Unsynchronized.ref
     1.8    val names_long_raw: Config.raw
     1.9    val names_long: bool Config.T
    1.10 -  val names_short_default: bool Unsynchronized.ref
    1.11    val names_short_raw: Config.raw
    1.12    val names_short: bool Config.T
    1.13 -  val names_unique_default: bool Unsynchronized.ref
    1.14    val names_unique_raw: Config.raw
    1.15    val names_unique: bool Config.T
    1.16    val extern: Proof.context -> T -> string -> xstring
    1.17 @@ -166,16 +163,13 @@
    1.18  fun intern space xname = #1 (lookup space xname);
    1.19  
    1.20  
    1.21 -val names_long_default = Unsynchronized.ref false;
    1.22 -val names_long_raw = Config.declare "names_long" (fn _ => Config.Bool (! names_long_default));
    1.23 +val names_long_raw = Config.declare_option "names_long";
    1.24  val names_long = Config.bool names_long_raw;
    1.25  
    1.26 -val names_short_default = Unsynchronized.ref false;
    1.27 -val names_short_raw = Config.declare "names_short" (fn _ => Config.Bool (! names_short_default));
    1.28 +val names_short_raw = Config.declare_option "names_short";
    1.29  val names_short = Config.bool names_short_raw;
    1.30  
    1.31 -val names_unique_default = Unsynchronized.ref true;
    1.32 -val names_unique_raw = Config.declare "names_unique" (fn _ => Config.Bool (! names_unique_default));
    1.33 +val names_unique_raw = Config.declare_option "names_unique";
    1.34  val names_unique = Config.bool names_unique_raw;
    1.35  
    1.36  fun extern ctxt space name =
     2.1 --- a/src/Pure/ProofGeneral/preferences.ML	Sun May 12 19:56:30 2013 +0200
     2.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Sun May 12 20:25:45 2013 +0200
     2.3 @@ -145,7 +145,7 @@
     2.4    bool_pref Goal_Display.show_consts_default
     2.5      "show-consts"
     2.6      "Show types of consts in Isabelle goal display",
     2.7 -  bool_pref Name_Space.names_long_default
     2.8 +  options_pref "names_long"
     2.9      "long-names"
    2.10      "Show fully qualified names in Isabelle terms",
    2.11    bool_pref Printer.show_brackets_default
    2.12 @@ -163,7 +163,7 @@
    2.13      "goals-limit"
    2.14      "Setting for maximum number of goals printed",
    2.15    print_depth_pref,
    2.16 -  bool_pref Printer.show_question_marks_default
    2.17 +  options_pref "show_question_marks"
    2.18      "show-question-marks"
    2.19      "Show leading question mark of variable name"];
    2.20  
     3.1 --- a/src/Pure/Syntax/printer.ML	Sun May 12 19:56:30 2013 +0200
     3.2 +++ b/src/Pure/Syntax/printer.ML	Sun May 12 20:25:45 2013 +0200
     3.3 @@ -29,7 +29,6 @@
     3.4    val show_markup_default: bool Unsynchronized.ref
     3.5    val show_markup_raw: Config.raw
     3.6    val show_structs_raw: Config.raw
     3.7 -  val show_question_marks_default: bool Unsynchronized.ref
     3.8    val show_question_marks_raw: Config.raw
     3.9    val show_type_constraint: Proof.context -> bool
    3.10    val show_sort_constraint: Proof.context -> bool
    3.11 @@ -77,9 +76,7 @@
    3.12  val show_structs_raw = Config.declare "show_structs" (fn _ => Config.Bool false);
    3.13  val show_structs = Config.bool show_structs_raw;
    3.14  
    3.15 -val show_question_marks_default = Unsynchronized.ref true;
    3.16 -val show_question_marks_raw =
    3.17 -  Config.declare "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
    3.18 +val show_question_marks_raw = Config.declare_option "show_question_marks";
    3.19  val show_question_marks = Config.bool show_question_marks_raw;
    3.20  
    3.21  fun show_type_constraint ctxt = Config.get ctxt show_types orelse Config.get ctxt show_markup;
     4.1 --- a/src/Pure/Tools/build.ML	Sun May 12 19:56:30 2013 +0200
     4.2 +++ b/src/Pure/Tools/build.ML	Sun May 12 20:25:45 2013 +0200
     4.3 @@ -93,11 +93,6 @@
     4.4      |> no_document options ? Present.no_document
     4.5      |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
     4.6      |> Unsynchronized.setmp Goal.skip_proofs (Options.bool options "skip_proofs")
     4.7 -    |> Unsynchronized.setmp Printer.show_question_marks_default
     4.8 -        (Options.bool options "show_question_marks")
     4.9 -    |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")
    4.10 -    |> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short")
    4.11 -    |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique")
    4.12      |> Unsynchronized.setmp Thy_Output.display_default (Options.bool options "thy_output_display")
    4.13      |> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes")
    4.14      |> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent")
     5.1 --- a/src/Tools/WWW_Find/Start_WWW_Find.thy	Sun May 12 19:56:30 2013 +0200
     5.2 +++ b/src/Tools/WWW_Find/Start_WWW_Find.thy	Sun May 12 20:25:45 2013 +0200
     5.3 @@ -5,6 +5,7 @@
     5.4  theory Start_WWW_Find imports WWW_Find begin
     5.5  
     5.6  ML {*
     5.7 +  Options.default_put_bool "show_question_marks" false;
     5.8    YXML_Find_Theorems.init ();
     5.9    val port = OS.Process.getEnv "SCGIPORT" |> the |> Int.fromString |> the;
    5.10    ScgiServer.server' 10 "/" port;
     6.1 --- a/src/Tools/WWW_Find/find_theorems.ML	Sun May 12 19:56:30 2013 +0200
     6.2 +++ b/src/Tools/WWW_Find/find_theorems.ML	Sun May 12 20:25:45 2013 +0200
     6.3 @@ -55,7 +55,6 @@
     6.4    end;
     6.5  in
     6.6  
     6.7 -val () = Printer.show_question_marks_default := false;
     6.8  val () = ScgiServer.register ("find_theorems", SOME Mime.html, ScgiServer.simple_handler find_theorems);
     6.9  
    6.10  end;