src/Doc/Isar_Ref/Document_Preparation.thy
changeset 67219 81e9804b2014
parent 67139 8fe0aba577af
child 67263 449a989f42cd
     1.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Sat Dec 16 20:02:40 2017 +0100
     1.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Sat Dec 16 21:53:07 2017 +0100
     1.3 @@ -107,6 +107,7 @@
     1.4      @{antiquotation_def emph} & : & \<open>antiquotation\<close> \\
     1.5      @{antiquotation_def bold} & : & \<open>antiquotation\<close> \\
     1.6      @{antiquotation_def verbatim} & : & \<open>antiquotation\<close> \\
     1.7 +    @{antiquotation_def session} & : & \<open>antiquotation\<close> \\
     1.8      @{antiquotation_def "file"} & : & \<open>antiquotation\<close> \\
     1.9      @{antiquotation_def "url"} & : & \<open>antiquotation\<close> \\
    1.10      @{antiquotation_def "cite"} & : & \<open>antiquotation\<close> \\
    1.11 @@ -195,6 +196,7 @@
    1.12        @@{antiquotation emph} options @{syntax text} |
    1.13        @@{antiquotation bold} options @{syntax text} |
    1.14        @@{antiquotation verbatim} options @{syntax text} |
    1.15 +      @@{antiquotation session} options @{syntax embedded} |
    1.16        @@{antiquotation path} options @{syntax embedded} |
    1.17        @@{antiquotation "file"} options @{syntax name} |
    1.18        @@{antiquotation dir} options @{syntax name} |
    1.19 @@ -284,6 +286,9 @@
    1.20    \<^descr> \<open>@{verbatim s}\<close> prints uninterpreted source text literally as ASCII
    1.21    characters, using some type-writer font style.
    1.22  
    1.23 +  \<^descr> \<open>@{session name}\<close> prints given session name verbatim. The name is checked
    1.24 +  wrt.\ the dependencies of the current session.
    1.25 +
    1.26    \<^descr> \<open>@{path name}\<close> prints the file-system path name verbatim.
    1.27  
    1.28    \<^descr> \<open>@{file name}\<close> is like \<open>@{path name}\<close>, but ensures that \<open>name\<close> refers to a