tuned;
authorwenzelm
Thu Apr 17 11:42:36 2014 +0200 (2014-04-17)
changeset 56614d80f43dab30e
parent 56613 3518ea9f5200
child 56615 47c1dbeec36a
tuned;
src/Pure/Thy/present.ML
src/Pure/Tools/build.ML
     1.1 --- a/src/Pure/Thy/present.ML	Thu Apr 17 11:31:46 2014 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Thu Apr 17 11:42:36 2014 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  signature PRESENT =
     1.5  sig
     1.6    val session_name: theory -> string
     1.7 +  val document_enabled: string -> bool
     1.8    val document_variants: string -> (string * string) list
     1.9    val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
    1.10      (Path.T * Path.T) list -> string * string -> bool -> theory list -> unit  (*not thread-safe!*)
    1.11 @@ -192,7 +193,9 @@
    1.12  
    1.13  (** document preparation **)
    1.14  
    1.15 -(* document variants *)
    1.16 +(* options *)
    1.17 +
    1.18 +fun document_enabled s = s <> "" andalso s <> "false";
    1.19  
    1.20  fun document_variants str =
    1.21    let
     2.1 --- a/src/Pure/Tools/build.ML	Thu Apr 17 11:31:46 2014 +0200
     2.2 +++ b/src/Pure/Tools/build.ML	Thu Apr 17 11:42:36 2014 +0200
     2.3 @@ -99,8 +99,7 @@
     2.4  
     2.5  fun use_theories last_timing options =
     2.6    Thy_Info.use_theories {
     2.7 -      document =
     2.8 -        (case Options.string options "document" of "" => false | "false" => false | _ => true),
     2.9 +      document = Present.document_enabled (Options.string options "document"),
    2.10        last_timing = last_timing,
    2.11        master_dir = Path.current}
    2.12      |> Unsynchronized.setmp print_mode