added document antiquotation @{system_option};

--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Wed Nov 20 17:26:04 2019 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Nov 21 13:25:27 2019 +0100
@@ -108,6 +108,7 @@
     @{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> \\
@@ -198,6 +199,7 @@
       @@{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} |
@@ -290,6 +292,10 @@
   \<^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.
 

--- a/src/Pure/Thy/document_antiquotations.ML	Wed Nov 20 17:26:04 2019 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Thu Nov 21 13:25:27 2019 +0100
@@ -260,6 +260,16 @@
       in #1 (Input.source_content text) end));
 
 
+(* system options *)
+
+val _ = Theory.setup
+  (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>system_option\<close>
+    (Scan.lift Args.embedded_position)
+    (fn ctxt => fn (name, pos) =>
+      let val _ = Completion.check_option (Options.default ()) ctxt (name, pos);
+      in name end));
+
+
 (* ML text *)
 
 local