equal
deleted
inserted
replaced
123 * Document markers are formal comments of the form \<^marker>\<open>marker_body\<close> that |
123 * Document markers are formal comments of the form \<^marker>\<open>marker_body\<close> that |
124 are stripped from document output: the effect is to modify the semantic |
124 are stripped from document output: the effect is to modify the semantic |
125 presentation context or to emit markup to the PIDE document. Some |
125 presentation context or to emit markup to the PIDE document. Some |
126 predefined markers are taken from the Dublin Core Metadata Initiative, |
126 predefined markers are taken from the Dublin Core Metadata Initiative, |
127 e.g. \<^marker>\<open>contributor arg\<close> or \<^marker>\<open>license arg\<close> and produce PIDE markup that |
127 e.g. \<^marker>\<open>contributor arg\<close> or \<^marker>\<open>license arg\<close> and produce PIDE markup that |
128 can retrieved from the document database. |
128 can be retrieved from the document database. |
129 |
129 |
130 * Old-style command tags %name are re-interpreted as markers with |
130 * Old-style command tags %name are re-interpreted as markers with |
131 proof-scope \<^marker>\<open>tag (proof) name\<close> and produce LaTeX environments as |
131 proof-scope \<^marker>\<open>tag (proof) name\<close> and produce LaTeX environments as |
132 before. Potential INCOMPATIBILITY: multiple markers are composed in |
132 before. Potential INCOMPATIBILITY: multiple markers are composed in |
133 canonical order, resulting in a reversed list of tags in the |
133 canonical order, resulting in a reversed list of tags in the |