equal
deleted
inserted
replaced
105 @{antiquotation_def ML_structure} & : & \<open>antiquotation\<close> \\ |
105 @{antiquotation_def ML_structure} & : & \<open>antiquotation\<close> \\ |
106 @{antiquotation_def ML_functor} & : & \<open>antiquotation\<close> \\ |
106 @{antiquotation_def ML_functor} & : & \<open>antiquotation\<close> \\ |
107 @{antiquotation_def emph} & : & \<open>antiquotation\<close> \\ |
107 @{antiquotation_def emph} & : & \<open>antiquotation\<close> \\ |
108 @{antiquotation_def bold} & : & \<open>antiquotation\<close> \\ |
108 @{antiquotation_def bold} & : & \<open>antiquotation\<close> \\ |
109 @{antiquotation_def verbatim} & : & \<open>antiquotation\<close> \\ |
109 @{antiquotation_def verbatim} & : & \<open>antiquotation\<close> \\ |
|
110 @{antiquotation_def session} & : & \<open>antiquotation\<close> \\ |
110 @{antiquotation_def "file"} & : & \<open>antiquotation\<close> \\ |
111 @{antiquotation_def "file"} & : & \<open>antiquotation\<close> \\ |
111 @{antiquotation_def "url"} & : & \<open>antiquotation\<close> \\ |
112 @{antiquotation_def "url"} & : & \<open>antiquotation\<close> \\ |
112 @{antiquotation_def "cite"} & : & \<open>antiquotation\<close> \\ |
113 @{antiquotation_def "cite"} & : & \<open>antiquotation\<close> \\ |
113 @{command_def "print_antiquotations"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
114 @{command_def "print_antiquotations"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
114 \end{matharray} |
115 \end{matharray} |
193 @@{antiquotation ML_structure} options @{syntax text} | |
194 @@{antiquotation ML_structure} options @{syntax text} | |
194 @@{antiquotation ML_functor} options @{syntax text} | |
195 @@{antiquotation ML_functor} options @{syntax text} | |
195 @@{antiquotation emph} options @{syntax text} | |
196 @@{antiquotation emph} options @{syntax text} | |
196 @@{antiquotation bold} options @{syntax text} | |
197 @@{antiquotation bold} options @{syntax text} | |
197 @@{antiquotation verbatim} options @{syntax text} | |
198 @@{antiquotation verbatim} options @{syntax text} | |
|
199 @@{antiquotation session} options @{syntax embedded} | |
198 @@{antiquotation path} options @{syntax embedded} | |
200 @@{antiquotation path} options @{syntax embedded} | |
199 @@{antiquotation "file"} options @{syntax name} | |
201 @@{antiquotation "file"} options @{syntax name} | |
200 @@{antiquotation dir} options @{syntax name} | |
202 @@{antiquotation dir} options @{syntax name} | |
201 @@{antiquotation url} options @{syntax embedded} | |
203 @@{antiquotation url} options @{syntax embedded} | |
202 @@{antiquotation cite} options @{syntax cartouche}? (@{syntax name} + @'and') |
204 @@{antiquotation cite} options @{syntax cartouche}? (@{syntax name} + @'and') |
281 \<^descr> \<open>@{bold s}\<close> prints document source recursively, with {\LaTeX} markup |
283 \<^descr> \<open>@{bold s}\<close> prints document source recursively, with {\LaTeX} markup |
282 \<^verbatim>\<open>\textbf{\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close>. |
284 \<^verbatim>\<open>\textbf{\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close>. |
283 |
285 |
284 \<^descr> \<open>@{verbatim s}\<close> prints uninterpreted source text literally as ASCII |
286 \<^descr> \<open>@{verbatim s}\<close> prints uninterpreted source text literally as ASCII |
285 characters, using some type-writer font style. |
287 characters, using some type-writer font style. |
|
288 |
|
289 \<^descr> \<open>@{session name}\<close> prints given session name verbatim. The name is checked |
|
290 wrt.\ the dependencies of the current session. |
286 |
291 |
287 \<^descr> \<open>@{path name}\<close> prints the file-system path name verbatim. |
292 \<^descr> \<open>@{path name}\<close> prints the file-system path name verbatim. |
288 |
293 |
289 \<^descr> \<open>@{file name}\<close> is like \<open>@{path name}\<close>, but ensures that \<open>name\<close> refers to a |
294 \<^descr> \<open>@{file name}\<close> is like \<open>@{path name}\<close>, but ensures that \<open>name\<close> refers to a |
290 plain file. |
295 plain file. |