--- a/src/Doc/Isar_Ref/Document_Preparation.thy Wed May 27 13:57:13 2020 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Wed May 27 14:27:22 2020 +0200
@@ -108,6 +108,7 @@
@{antiquotation_def emph} & : & \<open>antiquotation\<close> \\
@{antiquotation_def bold} & : & \<open>antiquotation\<close> \\
@{antiquotation_def verbatim} & : & \<open>antiquotation\<close> \\
+ @{antiquotation_def bash_function} & : & \<open>antiquotation\<close> \\
@{antiquotation_def system_option} & : & \<open>antiquotation\<close> \\
@{antiquotation_def session} & : & \<open>antiquotation\<close> \\
@{antiquotation_def "file"} & : & \<open>antiquotation\<close> \\
@@ -199,6 +200,7 @@
@@{antiquotation emph} options @{syntax text} |
@@{antiquotation bold} options @{syntax text} |
@@{antiquotation verbatim} options @{syntax text} |
+ @@{antiquotation bash_function} options @{syntax embedded} |
@@{antiquotation system_option} options @{syntax embedded} |
@@{antiquotation session} options @{syntax embedded} |
@@{antiquotation path} options @{syntax embedded} |
@@ -292,6 +294,10 @@
\<^descr> \<open>@{verbatim s}\<close> prints uninterpreted source text literally as ASCII
characters, using some type-writer font style.
+ \<^descr> \<open>@{bash_function name}\<close> prints the given GNU bash function verbatim. The
+ name is checked wrt.\ the Isabelle system environment @{cite
+ "isabelle-system"}.
+
\<^descr> \<open>@{system_option name}\<close> prints the given system option verbatim. The name
is checked wrt.\ cumulative \<^verbatim>\<open>etc/options\<close> of all Isabelle components,
notably \<^file>\<open>~~/etc/options\<close>.