src/Doc/Isar_Ref/Document_Preparation.thy

       @@{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 path} options @{syntax name} |
       @@{antiquotation "file"} options @{syntax name} |
-      @@{antiquotation file_unchecked} options @{syntax name} |
+      @@{antiquotation dir} options @{syntax name} |
       @@{antiquotation url} options @{syntax embedded} |
       @@{antiquotation cite} options @{syntax cartouche}? (@{syntax name} + @'and')
     ;
     styles: '(' (style + ',') ')'
     ;

   \<^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>@{file path}\<close> checks that \<open>path\<close> refers to a file (or directory) and
-  prints it verbatim.
-
-  \<^descr> \<open>@{file_unchecked path}\<close> is like \<open>@{file path}\<close>, but does not check the
-  existence of the \<open>path\<close> within the file-system.
+  \<^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
+  plain file.
+
+  \<^descr> \<open>@{dir name}\<close> is like \<open>@{path name}\<close>, but ensures that \<open>name\<close> refers to a
+  directory.
 
   \<^descr> \<open>@{url name}\<close> produces markup for the given URL, which results in an
   active hyperlink within the text.
 
   \<^descr> \<open>@{cite name}\<close> produces a citation \<^verbatim>\<open>\cite{name}\<close> in {\LaTeX}, where the