# HG changeset patch
# User wenzelm
# Date 1598976197 -7200
# Node ID a5bf0b69c22a9ef716299dcf8d32744b4f12e743
# Parent  4d615ec4b6b1b85d17d9375bc404ce3ef87a2517
discontinue export_document --- always enabled (reverting f0f83ce0badd);

diff -r 4d615ec4b6b1 -r a5bf0b69c22a etc/options
--- a/etc/options	Tue Sep 01 17:51:20 2020 +0200
+++ b/etc/options	Tue Sep 01 18:03:17 2020 +0200
@@ -297,9 +297,6 @@
 
 section "Theory Export"
 
-option export_document : bool = false
-  -- "export document sources to Isabelle/Scala"
-
 option export_theory : bool = false
   -- "export theory content to Isabelle/Scala"
 
diff -r 4d615ec4b6b1 -r a5bf0b69c22a src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Sep 01 17:51:20 2020 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Sep 01 18:03:17 2020 +0200
@@ -68,10 +68,7 @@
           let
             val latex = Latex.isabelle_body (Context.theory_name thy) body;
             val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
-            val _ =
-              if Options.bool options "export_document" then
-                Export.export thy (Path.explode_binding0 "document.tex") (XML.blob output)
-              else ();
+            val _ = Export.export thy (Path.explode_binding0 "document.tex") (XML.blob output);
             val _ = if #enabled option then Present.theory_output thy output else ();
           in () end
       end));
diff -r 4d615ec4b6b1 -r a5bf0b69c22a src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Tue Sep 01 17:51:20 2020 +0200
+++ b/src/Pure/Tools/dump.scala	Tue Sep 01 18:03:17 2020 +0200
@@ -61,7 +61,7 @@
         { case args =>
             for (entry <- args.snapshot.exports if entry.name == "document.tex")
               args.write(Path.explode(entry.name), entry.uncompressed())
-        }, options = List("export_document")),
+        }),
       Aspect("theory", "foundational theory content",
         { case args =>
             for {