diff -r d0c1b2dbca5b -r 5bf08c9aa036 src/Doc/Isar_Ref/Document_Preparation.thy --- a/src/Doc/Isar_Ref/Document_Preparation.thy Wed Apr 13 11:26:52 2016 +0200 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy Wed Apr 13 11:31:13 2016 +0200 @@ -195,8 +195,8 @@ @@{antiquotation emph} options @{syntax text} | @@{antiquotation bold} options @{syntax text} | @@{antiquotation verbatim} options @{syntax text} | - @@{antiquotation "file"} options @{syntax name} | - @@{antiquotation file_unchecked} options @{syntax name} | + @@{antiquotation "file"} options @{syntax xname} | + @@{antiquotation file_unchecked} options @{syntax xname} | @@{antiquotation url} options @{syntax name} | @@{antiquotation cite} options @{syntax cartouche}? (@{syntax name} + @'and') ; @@ -613,7 +613,7 @@ \end{matharray} @{rail \ - @@{command display_drafts} (@{syntax name} +) + @@{command display_drafts} (@{syntax xname} +) \} \<^descr> @{command "display_drafts"}~\paths\ performs simple output of a given list