--- a/src/Doc/ROOT Mon May 25 22:37:14 2020 +0200
+++ b/src/Doc/ROOT Mon May 25 22:37:22 2020 +0200
@@ -378,7 +378,7 @@
"root.tex"
session System (doc) in "System" = Pure +
- options [document_variants = "system", thy_output_source]
+ options [document_variants = "system", thy_output_source, pide_session]
sessions
"HOL-Library"
theories
--- a/src/Doc/System/Sessions.thy Mon May 25 22:37:14 2020 +0200
+++ b/src/Doc/System/Sessions.thy Mon May 25 22:37:22 2020 +0200
@@ -578,10 +578,10 @@
\<^medskip> Option \<^verbatim>\<open>-A\<close> specifies named aspects of the dump, as a comma-separated
list. The default is to dump all known aspects, as given in the command-line
- usage of the tool. The underlying Isabelle/Scala function
- \<^verbatim>\<open>isabelle.Dump.dump()\<close> takes aspects as user-defined operations on the
- final PIDE state and document version. This allows to imitate Prover IDE
- rendering under program control.
+ usage of the tool. The underlying Isabelle/Scala operation
+ \<^scala_method>\<open>isabelle.Dump.dump\<close> takes aspects as user-defined
+ operations on the final PIDE state and document version. This allows to
+ imitate Prover IDE rendering under program control.
\<close>