# HG changeset patch
# User wenzelm
# Date 1590439042 -7200
# Node ID a27747c857007e5f14d6f57127d386b1f6b32ae3
# Parent  dff81ce866d4fed4ec80c72413d68537c332fe90
more antiquotations;

diff -r dff81ce866d4 -r a27747c85700 src/Doc/ROOT
--- 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
diff -r dff81ce866d4 -r a27747c85700 src/Doc/System/Sessions.thy
--- 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>