# HG changeset patch
# User wenzelm
# Date 1343157988 -7200
# Node ID 691d0b44a79312f0e38e5a75e54138570d16acc6
# Parent  2cbc3d284cd8f1bb9f00fe6d8804ec4592ec37b5
more build options;

diff -r 2cbc3d284cd8 -r 691d0b44a793 etc/options
--- a/etc/options	Tue Jul 24 21:07:54 2012 +0200
+++ b/etc/options	Tue Jul 24 21:26:28 2012 +0200
@@ -22,3 +22,9 @@
 
 declare condition : string = ""
 
+declare show_question_marks : bool = true
+
+declare names_long : bool = false
+declare names_short : bool = false
+declare names_unique : bool = true
+
diff -r 2cbc3d284cd8 -r 691d0b44a793 src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Jul 24 21:07:54 2012 +0200
+++ b/src/HOL/ROOT	Tue Jul 24 21:26:28 2012 +0200
@@ -693,7 +693,7 @@
     "RIPEMD-160/rmd/s_r.siv"
 
 session Manual in "SPARK/Manual" = "HOL-SPARK" +
-  (* FIXME Printer.show_question_marks_default := false; *)
+  options [show_question_marks = false]
   theories
     Example_Verification
     VC_Principles
diff -r 2cbc3d284cd8 -r 691d0b44a793 src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Tue Jul 24 21:07:54 2012 +0200
+++ b/src/Pure/System/build.ML	Tue Jul 24 21:26:28 2012 +0200
@@ -26,7 +26,12 @@
     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
     |> (case Options.string options "document" of "" => true | "false" => true | _ => false) ?
         Present.no_document
-    |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty");
+    |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
+    |> 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");
 
 fun use_theories (options, thys) =
   let val condition = space_explode "," (Options.string options "condition") in