disable export_document by default (presently unused and for demo/testing purposes): avoid spurious IO exception in highly parallel environment;
authorwenzelm
Sun Jun 24 22:13:23 2018 +0200 (14 months ago)
changeset 68491f0f83ce0badd
parent 68490 eb53f944c8cd
child 68492 c7e0a7bcacaf
child 68493 143b4cc8fc74
disable export_document by default (presently unused and for demo/testing purposes): avoid spurious IO exception in highly parallel environment;
etc/options
src/Pure/Thy/thy_info.ML
src/Pure/Tools/dump.scala
     1.1 --- a/etc/options	Sun Jun 24 15:57:48 2018 +0200
     1.2 +++ b/etc/options	Sun Jun 24 22:13:23 2018 +0200
     1.3 @@ -252,6 +252,8 @@
     1.4  
     1.5  section "Theory Export"
     1.6  
     1.7 +option export_document : bool = false
     1.8 +
     1.9  option export_theory : bool = false
    1.10  
    1.11  
     2.1 --- a/src/Pure/Thy/thy_info.ML	Sun Jun 24 15:57:48 2018 +0200
     2.2 +++ b/src/Pure/Thy/thy_info.ML	Sun Jun 24 22:13:23 2018 +0200
     2.3 @@ -64,7 +64,9 @@
     2.4            let
     2.5              val latex = Latex.isabelle_body (Context.theory_name thy) body;
     2.6              val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
     2.7 -            val _ = Export.export thy "document.tex" output;
     2.8 +            val _ =
     2.9 +              if Options.bool options "export_document"
    2.10 +              then Export.export thy "document.tex" output else ();
    2.11              val _ = if #enabled option then Present.theory_output thy output else ();
    2.12            in () end
    2.13        end));
     3.1 --- a/src/Pure/Tools/dump.scala	Sun Jun 24 15:57:48 2018 +0200
     3.2 +++ b/src/Pure/Tools/dump.scala	Sun Jun 24 22:13:23 2018 +0200
     3.3 @@ -56,7 +56,7 @@
     3.4          { case args =>
     3.5              for (entry <- args.snapshot.exports if entry.name == "document.tex")
     3.6                args.write(Path.explode(entry.name), entry.uncompressed())
     3.7 -        }, options = List("editor_presentation")),
     3.8 +        }, options = List("editor_presentation", "export_document")),
     3.9        Aspect("theory", "foundational theory content",
    3.10          { case args =>
    3.11              for {