more build options;
authorwenzelm
Tue Jul 24 21:26:28 2012 +0200 (2012-07-24)
changeset 48486691d0b44a793
parent 48485 2cbc3d284cd8
child 48487 94a9650f79fb
more build options;
etc/options
src/HOL/ROOT
src/Pure/System/build.ML
     1.1 --- a/etc/options	Tue Jul 24 21:07:54 2012 +0200
     1.2 +++ b/etc/options	Tue Jul 24 21:26:28 2012 +0200
     1.3 @@ -22,3 +22,9 @@
     1.4  
     1.5  declare condition : string = ""
     1.6  
     1.7 +declare show_question_marks : bool = true
     1.8 +
     1.9 +declare names_long : bool = false
    1.10 +declare names_short : bool = false
    1.11 +declare names_unique : bool = true
    1.12 +
     2.1 --- a/src/HOL/ROOT	Tue Jul 24 21:07:54 2012 +0200
     2.2 +++ b/src/HOL/ROOT	Tue Jul 24 21:26:28 2012 +0200
     2.3 @@ -693,7 +693,7 @@
     2.4      "RIPEMD-160/rmd/s_r.siv"
     2.5  
     2.6  session Manual in "SPARK/Manual" = "HOL-SPARK" +
     2.7 -  (* FIXME Printer.show_question_marks_default := false; *)
     2.8 +  options [show_question_marks = false]
     2.9    theories
    2.10      Example_Verification
    2.11      VC_Principles
     3.1 --- a/src/Pure/System/build.ML	Tue Jul 24 21:07:54 2012 +0200
     3.2 +++ b/src/Pure/System/build.ML	Tue Jul 24 21:26:28 2012 +0200
     3.3 @@ -26,7 +26,12 @@
     3.4      |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
     3.5      |> (case Options.string options "document" of "" => true | "false" => true | _ => false) ?
     3.6          Present.no_document
     3.7 -    |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty");
     3.8 +    |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
     3.9 +    |> Unsynchronized.setmp Printer.show_question_marks_default
    3.10 +        (Options.bool options "show_question_marks")
    3.11 +    |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")
    3.12 +    |> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short")
    3.13 +    |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique");
    3.14  
    3.15  fun use_theories (options, thys) =
    3.16    let val condition = space_explode "," (Options.string options "condition") in