equal
deleted
inserted
replaced
106 @{antiquotation_def ML_structure} & : & \<open>antiquotation\<close> \\ |
106 @{antiquotation_def ML_structure} & : & \<open>antiquotation\<close> \\ |
107 @{antiquotation_def ML_functor} & : & \<open>antiquotation\<close> \\ |
107 @{antiquotation_def ML_functor} & : & \<open>antiquotation\<close> \\ |
108 @{antiquotation_def emph} & : & \<open>antiquotation\<close> \\ |
108 @{antiquotation_def emph} & : & \<open>antiquotation\<close> \\ |
109 @{antiquotation_def bold} & : & \<open>antiquotation\<close> \\ |
109 @{antiquotation_def bold} & : & \<open>antiquotation\<close> \\ |
110 @{antiquotation_def verbatim} & : & \<open>antiquotation\<close> \\ |
110 @{antiquotation_def verbatim} & : & \<open>antiquotation\<close> \\ |
|
111 @{antiquotation_def bash_function} & : & \<open>antiquotation\<close> \\ |
111 @{antiquotation_def system_option} & : & \<open>antiquotation\<close> \\ |
112 @{antiquotation_def system_option} & : & \<open>antiquotation\<close> \\ |
112 @{antiquotation_def session} & : & \<open>antiquotation\<close> \\ |
113 @{antiquotation_def session} & : & \<open>antiquotation\<close> \\ |
113 @{antiquotation_def "file"} & : & \<open>antiquotation\<close> \\ |
114 @{antiquotation_def "file"} & : & \<open>antiquotation\<close> \\ |
114 @{antiquotation_def "url"} & : & \<open>antiquotation\<close> \\ |
115 @{antiquotation_def "url"} & : & \<open>antiquotation\<close> \\ |
115 @{antiquotation_def "cite"} & : & \<open>antiquotation\<close> \\ |
116 @{antiquotation_def "cite"} & : & \<open>antiquotation\<close> \\ |
197 @@{antiquotation ML_structure} options @{syntax text} | |
198 @@{antiquotation ML_structure} options @{syntax text} | |
198 @@{antiquotation ML_functor} options @{syntax text} | |
199 @@{antiquotation ML_functor} options @{syntax text} | |
199 @@{antiquotation emph} options @{syntax text} | |
200 @@{antiquotation emph} options @{syntax text} | |
200 @@{antiquotation bold} options @{syntax text} | |
201 @@{antiquotation bold} options @{syntax text} | |
201 @@{antiquotation verbatim} options @{syntax text} | |
202 @@{antiquotation verbatim} options @{syntax text} | |
|
203 @@{antiquotation bash_function} options @{syntax embedded} | |
202 @@{antiquotation system_option} options @{syntax embedded} | |
204 @@{antiquotation system_option} options @{syntax embedded} | |
203 @@{antiquotation session} options @{syntax embedded} | |
205 @@{antiquotation session} options @{syntax embedded} | |
204 @@{antiquotation path} options @{syntax embedded} | |
206 @@{antiquotation path} options @{syntax embedded} | |
205 @@{antiquotation "file"} options @{syntax name} | |
207 @@{antiquotation "file"} options @{syntax name} | |
206 @@{antiquotation dir} options @{syntax name} | |
208 @@{antiquotation dir} options @{syntax name} | |
289 \<^descr> \<open>@{bold s}\<close> prints document source recursively, with {\LaTeX} markup |
291 \<^descr> \<open>@{bold s}\<close> prints document source recursively, with {\LaTeX} markup |
290 \<^verbatim>\<open>\textbf{\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close>. |
292 \<^verbatim>\<open>\textbf{\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close>. |
291 |
293 |
292 \<^descr> \<open>@{verbatim s}\<close> prints uninterpreted source text literally as ASCII |
294 \<^descr> \<open>@{verbatim s}\<close> prints uninterpreted source text literally as ASCII |
293 characters, using some type-writer font style. |
295 characters, using some type-writer font style. |
|
296 |
|
297 \<^descr> \<open>@{bash_function name}\<close> prints the given GNU bash function verbatim. The |
|
298 name is checked wrt.\ the Isabelle system environment @{cite |
|
299 "isabelle-system"}. |
294 |
300 |
295 \<^descr> \<open>@{system_option name}\<close> prints the given system option verbatim. The name |
301 \<^descr> \<open>@{system_option name}\<close> prints the given system option verbatim. The name |
296 is checked wrt.\ cumulative \<^verbatim>\<open>etc/options\<close> of all Isabelle components, |
302 is checked wrt.\ cumulative \<^verbatim>\<open>etc/options\<close> of all Isabelle components, |
297 notably \<^file>\<open>~~/etc/options\<close>. |
303 notably \<^file>\<open>~~/etc/options\<close>. |
298 |
304 |