src/Pure/Thy/present.ML

 *)
 
 signature PRESENT =
 sig
   val session_name: theory -> string
+  val document_enabled: string -> bool
   val document_variants: string -> (string * string) list
   val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     (Path.T * Path.T) list -> string * string -> bool -> theory list -> unit  (*not thread-safe!*)
   val finish: unit -> unit  (*not thread-safe!*)
   val theory_output: string -> string -> unit

 
 
 
 (** document preparation **)
 
-(* document variants *)
+(* options *)
+
+fun document_enabled s = s <> "" andalso s <> "false";
 
 fun document_variants str =
   let
     fun read_variant s =
       (case space_explode "=" s of