76 * There is a new short form for antiquotations with a single argument |
76 * There is a new short form for antiquotations with a single argument |
77 that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and |
77 that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and |
78 \<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. The |
78 \<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. The |
79 standard Isabelle fonts provide glyphs to render important control |
79 standard Isabelle fonts provide glyphs to render important control |
80 symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>". |
80 symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>". |
|
81 |
|
82 * System option "document_symbols" determines completion of Isabelle |
|
83 symbols within document source. |
81 |
84 |
82 * Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}. |
85 * Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}. |
83 Consequently, \<open>...\<close> without any decoration prints literal quasi-formal |
86 Consequently, \<open>...\<close> without any decoration prints literal quasi-formal |
84 text. Command-line tool "isabelle update_cartouches -t" helps to update |
87 text. Command-line tool "isabelle update_cartouches -t" helps to update |
85 old sources, by approximative patching of the content of string and |
88 old sources, by approximative patching of the content of string and |