src/Doc/Isar_Ref/Document_Preparation.thy

     @{antiquotation_def ML_structure} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def ML_functor} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def emph} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def bold} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def verbatim} & : & \<open>antiquotation\<close> \\
+    @{antiquotation_def system_option} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def session} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def "file"} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def "url"} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def "cite"} & : & \<open>antiquotation\<close> \\
     @{command_def "print_antiquotations"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\

       @@{antiquotation ML_structure} options @{syntax text} |
       @@{antiquotation ML_functor} options @{syntax text} |
       @@{antiquotation emph} options @{syntax text} |
       @@{antiquotation bold} options @{syntax text} |
       @@{antiquotation verbatim} options @{syntax text} |
+      @@{antiquotation system_option} options @{syntax embedded} |
       @@{antiquotation session} options @{syntax embedded} |
       @@{antiquotation path} options @{syntax embedded} |
       @@{antiquotation "file"} options @{syntax name} |
       @@{antiquotation dir} options @{syntax name} |
       @@{antiquotation url} options @{syntax embedded} |

   \<^descr> \<open>@{bold s}\<close> prints document source recursively, with {\LaTeX} markup
   \<^verbatim>\<open>\textbf{\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close>.
 
   \<^descr> \<open>@{verbatim s}\<close> prints uninterpreted source text literally as ASCII
   characters, using some type-writer font style.
+
+  \<^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>.
 
   \<^descr> \<open>@{session name}\<close> prints given session name verbatim. The name is checked
   wrt.\ the dependencies of the current session.
 
   \<^descr> \<open>@{path name}\<close> prints the file-system path name verbatim.