src/Pure/Thy/thy_info.ML

         if #disabled option then ()
         else
           let
             val latex = Latex.isabelle_body (Context.theory_name thy) body;
             val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
-            val _ = Export.export thy "document.tex" output;
+            val _ =
+              if Options.bool options "export_document"
+              then Export.export thy "document.tex" output else ();
             val _ = if #enabled option then Present.theory_output thy output else ();
           in () end
       end));