equal
deleted
inserted
replaced
875 configuration, "-Djdk.gtk.version=3" might work better or worse. |
875 configuration, "-Djdk.gtk.version=3" might work better or worse. |
876 |
876 |
877 |
877 |
878 *** Document preparation *** |
878 *** Document preparation *** |
879 |
879 |
880 * High-quality blackboard-bold symbols from font "txmia" (package |
880 * High-quality blackboard-bold symbols for A..Z, from font "txmia" |
881 "txfonts"), for A..Z. |
881 (package "pxfonts"). |
882 |
882 |
883 * Document markers are formal comments of the form \<^marker>\<open>marker_body\<close> that |
883 * Document markers are formal comments of the form \<^marker>\<open>marker_body\<close> that |
884 are stripped from document output: the effect is to modify the semantic |
884 are stripped from document output: the effect is to modify the semantic |
885 presentation context or to emit markup to the PIDE document. Some |
885 presentation context or to emit markup to the PIDE document. Some |
886 predefined markers are taken from the Dublin Core Metadata Initiative, |
886 predefined markers are taken from the Dublin Core Metadata Initiative, |