235 \<^item> @{system_option_def "document_tags"} specifies alternative command tags |
235 \<^item> @{system_option_def "document_tags"} specifies alternative command tags |
236 as a comma-separated list of items: either ``\<open>command\<close>\<^verbatim>\<open>%\<close>\<open>tag\<close>'' for a |
236 as a comma-separated list of items: either ``\<open>command\<close>\<^verbatim>\<open>%\<close>\<open>tag\<close>'' for a |
237 specific command, or ``\<^verbatim>\<open>%\<close>\<open>tag\<close>'' as default for all other commands. This |
237 specific command, or ``\<^verbatim>\<open>%\<close>\<open>tag\<close>'' as default for all other commands. This |
238 is occasionally useful to control the global visibility of commands via |
238 is occasionally useful to control the global visibility of commands via |
239 session options (e.g.\ in \<^verbatim>\<open>ROOT\<close>). |
239 session options (e.g.\ in \<^verbatim>\<open>ROOT\<close>). |
|
240 |
|
241 \<^item> @{system_option_def "document_preprocessor"} specifies the name of an |
|
242 executable that is run within the document output directory, after |
|
243 preparing the document sources and before the actual build process. This |
|
244 allows to apply adhoc patches, without requiring a separate \<^verbatim>\<open>build\<close> |
|
245 script. |
240 |
246 |
241 \<^item> @{system_option_def "threads"} determines the number of worker threads |
247 \<^item> @{system_option_def "threads"} determines the number of worker threads |
242 for parallel checking of theories and proofs. The default \<open>0\<close> means that a |
248 for parallel checking of theories and proofs. The default \<open>0\<close> means that a |
243 sensible maximum value is determined by the underlying hardware. For |
249 sensible maximum value is determined by the underlying hardware. For |
244 machines with many cores or with hyperthreading, this is often requires |
250 machines with many cores or with hyperthreading, this is often requires |