# HG changeset patch
# User wenzelm
# Date 1529871203 -7200
# Node ID f0f83ce0badd797fed176e5e385949e65114a74a
# Parent  eb53f944c8cd35ad189aebb7f2c535efe8cf84d3
disable export_document by default (presently unused and for demo/testing purposes): avoid spurious IO exception in highly parallel environment;

diff -r eb53f944c8cd -r f0f83ce0badd etc/options
--- a/etc/options	Sun Jun 24 15:57:48 2018 +0200
+++ b/etc/options	Sun Jun 24 22:13:23 2018 +0200
@@ -252,6 +252,8 @@
 
 section "Theory Export"
 
+option export_document : bool = false
+
 option export_theory : bool = false
 
 
diff -r eb53f944c8cd -r f0f83ce0badd src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sun Jun 24 15:57:48 2018 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sun Jun 24 22:13:23 2018 +0200
@@ -64,7 +64,9 @@
           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));
diff -r eb53f944c8cd -r f0f83ce0badd src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Sun Jun 24 15:57:48 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Sun Jun 24 22:13:23 2018 +0200
@@ -56,7 +56,7 @@
         { case args =>
             for (entry <- args.snapshot.exports if entry.name == "document.tex")
               args.write(Path.explode(entry.name), entry.uncompressed())
-        }, options = List("editor_presentation")),
+        }, options = List("editor_presentation", "export_document")),
       Aspect("theory", "foundational theory content",
         { case args =>
             for {