# HG changeset patch
# User wenzelm
# Date 1673781199 -3600
# Node ID 90fea73f051d37d61462e76021d135bd9bf3f349
# Parent  6106c5b4e6eba3ca62074eccd9783f7165d1307b
more index entries;

diff -r 6106c5b4e6eb -r 90fea73f051d src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sun Jan 15 12:11:25 2023 +0100
+++ b/src/Doc/System/Sessions.thy	Sun Jan 15 12:13:19 2023 +0100
@@ -809,9 +809,9 @@
 
   \<^medskip> The following \<^verbatim>\<open>update\<close> options are supported:
 
-    \<^item> @{system_option update_inner_syntax_cartouches} to update inner syntax
-    (types, terms, etc.)~to use cartouches, instead of double-quoted strings
-    or atomic identifiers. For example, ``\<^theory_text>\<open>lemma \<doublequote>x =
+    \<^item> @{system_option_ref update_inner_syntax_cartouches} to update inner
+    syntax (types, terms, etc.)~to use cartouches, instead of double-quoted
+    strings or atomic identifiers. For example, ``\<^theory_text>\<open>lemma \<doublequote>x =
     x\<doublequote>\<close>'' is replaced by ``\<^theory_text>\<open>lemma \<open>x = x\<close>\<close>'', and ``\<^theory_text>\<open>assume
     A\<close>'' is replaced by ``\<^theory_text>\<open>assume \<open>A\<close>\<close>''.
 
@@ -820,17 +820,17 @@
     \<doublequote>+\<doublequote> 65)\<close>'' is replaced by ``\<^theory_text>\<open>(infixl \<open>+\<close>
     65)\<close>''.
 
-    \<^item> @{system_option update_control_cartouches} to update antiquotations to
-    use the compact form with control symbol and cartouche argument. For
+    \<^item> @{system_option_ref update_control_cartouches} to update antiquotations
+    to use the compact form with control symbol and cartouche argument. For
     example, ``\<open>@{term \<doublequote>x + y\<doublequote>}\<close>'' is replaced by
     ``\<open>\<^term>\<open>x + y\<close>\<close>'' (the control symbol is literally \<^verbatim>\<open>\<^term>\<close>.)
 
-    \<^item> @{system_option update_path_cartouches} to update file-system paths to
-    use cartouches: this depends on language markup provided by semantic
+    \<^item> @{system_option_ref update_path_cartouches} to update file-system paths
+    to use cartouches: this depends on language markup provided by semantic
     processing of parsed input.
 
-    \<^item> @{system_option update_cite} to update {\LaTeX} \<^verbatim>\<open>\cite\<close> commands and
-    old-style \<^verbatim>\<open>@{cite "name"}\<close> document antiquotations.
+    \<^item> @{system_option_ref update_cite} to update {\LaTeX} \<^verbatim>\<open>\cite\<close> commands
+    and old-style \<^verbatim>\<open>@{cite "name"}\<close> document antiquotations.
 
   It is also possible to produce custom updates in Isabelle/ML, by reporting
   \<^ML>\<open>Markup.update\<close> with the precise source position and a replacement