equal
deleted
inserted
replaced
14 |
14 |
15 Document antiquotations can be used for ensuring consistent type-setting of |
15 Document antiquotations can be used for ensuring consistent type-setting of |
16 various entities in a document. They can also be used for sophisticated |
16 various entities in a document. They can also be used for sophisticated |
17 \LaTeX-hacking. If you type @{text "Ctrl-c Ctrl-a h A"} inside ProofGeneral, you |
17 \LaTeX-hacking. If you type @{text "Ctrl-c Ctrl-a h A"} inside ProofGeneral, you |
18 obtain a list of all currently available document antiquotations and their options. |
18 obtain a list of all currently available document antiquotations and their options. |
|
19 You obtain the same list on the ML-level by typing |
|
20 |
|
21 @{ML [display,gray] "ThyOutput.print_antiquotations ()"} |
19 |
22 |
20 Below we give the code for two additional antiquotations that can be used to typeset |
23 Below we give the code for two additional antiquotations that can be used to typeset |
21 ML-code and also to check whether the given code actually compiles. This |
24 ML-code and also to check whether the given code actually compiles. This |
22 provides a sanity check for the code and also allows one to keep documents |
25 provides a sanity check for the code and also allows one to keep documents |
23 in sync with other code, for example Isabelle. |
26 in sync with other code, for example Isabelle. |