discontinue export_document --- always enabled (reverting f0f83ce0badd);

--- 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"
 

--- 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));

--- 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 {