src/Doc/System/Sessions.thy

   in particular with document preparation (\chref{ch:present}).
 
     \<^item> @{system_option_def "browser_info"} controls output of HTML browser
     info, see also \secref{sec:info}.
 
-    \<^item> @{system_option_def "document"} specifies the document output format,
-    see @{tool document} option \<^verbatim>\<open>-o\<close> in \secref{sec:tool-document}. In
-    practice, the most relevant values are \<^verbatim>\<open>document=false\<close> or
-    \<^verbatim>\<open>document=pdf\<close>.
+    \<^item> @{system_option_def "document"} controls document output for a
+    particular session or theory; \<^verbatim>\<open>document=pdf\<close> means enabled,
+    \<^verbatim>\<open>document=false\<close> means disabled (especially for particular theories).
 
     \<^item> @{system_option_def "document_output"} specifies an alternative
     directory for generated output of the document preparation system; the
     default is within the @{setting "ISABELLE_BROWSER_INFO"} hierarchy as
     explained in \secref{sec:info}. See also @{tool mkroot}, which generates a
     default configuration with output readily available to the author of the
     document.
 
     \<^item> @{system_option_def "document_variants"} specifies document variants as
-    a colon-separated list of \<open>name=tags\<close> entries, corresponding to @{tool
-    document} options \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-t\<close>.
-
-    For example, \<^verbatim>\<open>document_variants=document:outline=/proof,/ML\<close> indicates
+    a colon-separated list of \<open>name=tags\<close> entries. The default name
+    \<^verbatim>\<open>document\<close>, without additional tags.
+
+    Tags are specified as a comma separated list of modifier/name pairs and
+    tell {\LaTeX} how to interpret certain Isabelle command regions:
+    ``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'') means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to drop,
+    and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is
+    equivalent to the tag specification
+    ``\<^verbatim>\<open>+document,+theory,+proof,+ML,+visible,-invisible,+important,+unimportant\<close>'';
+    see also the {\LaTeX} macros \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and
+    \<^verbatim>\<open>\isafoldtag\<close>, in \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>.
+
+    In contrast, \<^verbatim>\<open>document_variants=document:outline=/proof,/ML\<close> indicates
     two documents: the one called \<^verbatim>\<open>document\<close> with default tags, and the other
     called \<^verbatim>\<open>outline\<close> where proofs and ML sections are folded.
 
     Document variant names are just a matter of conventions. It is also
     possible to use different document variant names (without tags) for