--- a/src/Doc/Isar_Ref/Document_Preparation.thy Sat Dec 16 20:02:40 2017 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Sat Dec 16 21:53:07 2017 +0100
@@ -107,6 +107,7 @@
@{antiquotation_def emph} & : & \<open>antiquotation\<close> \\
@{antiquotation_def bold} & : & \<open>antiquotation\<close> \\
@{antiquotation_def verbatim} & : & \<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> \\
@@ -195,6 +196,7 @@
@@{antiquotation emph} options @{syntax text} |
@@{antiquotation bold} options @{syntax text} |
@@{antiquotation verbatim} options @{syntax text} |
+ @@{antiquotation session} options @{syntax embedded} |
@@{antiquotation path} options @{syntax embedded} |
@@{antiquotation "file"} options @{syntax name} |
@@{antiquotation dir} options @{syntax name} |
@@ -284,6 +286,9 @@
\<^descr> \<open>@{verbatim s}\<close> prints uninterpreted source text literally as ASCII
characters, using some type-writer font style.
+ \<^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.
\<^descr> \<open>@{file name}\<close> is like \<open>@{path name}\<close>, but ensures that \<open>name\<close> refers to a