clarified no_document situation;
authorwenzelm
Wed, 25 Jul 2012 16:41:02 +0200
changeset 49515bf7f434b91d7
parent 49514 d648225071dd
child 49516 e59778bc71a0
clarified no_document situation;
src/Pure/System/build.ML
     1.1 --- a/src/Pure/System/build.ML	Wed Jul 25 12:40:17 2012 +0200
     1.2 +++ b/src/Pure/System/build.ML	Wed Jul 25 16:41:02 2012 +0200
     1.3 @@ -14,6 +14,10 @@
     1.4  
     1.5  local
     1.6  
     1.7 +fun no_document options =
     1.8 +  (case Options.string options "document" of "" => true | "false" => true | _ => false) andalso
     1.9 +  (Options.string options "document_dump" = "");
    1.10 +
    1.11  fun use_thys options =
    1.12    Thy_Info.use_thys
    1.13      |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
    1.14 @@ -24,8 +28,7 @@
    1.15          (Options.int options "parallel_proofs_threshold")
    1.16      |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    1.17      |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
    1.18 -    |> (case Options.string options "document" of "" => true | "false" => true | _ => false) ?
    1.19 -        Present.no_document
    1.20 +    |> no_document options ? Present.no_document
    1.21      |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
    1.22      |> Unsynchronized.setmp Printer.show_question_marks_default
    1.23          (Options.bool options "show_question_marks")