732 \<^item> @{system_option update_control_cartouches} to update antiquotations to |
732 \<^item> @{system_option update_control_cartouches} to update antiquotations to |
733 use the compact form with control symbol and cartouche argument. For |
733 use the compact form with control symbol and cartouche argument. For |
734 example, ``\<open>@{term \<doublequote>x + y\<doublequote>}\<close>'' is replaced by |
734 example, ``\<open>@{term \<doublequote>x + y\<doublequote>}\<close>'' is replaced by |
735 ``\<open>\<^term>\<open>x + y\<close>\<close>'' (the control symbol is literally \<^verbatim>\<open>\<^term>\<close>.) |
735 ``\<open>\<^term>\<open>x + y\<close>\<close>'' (the control symbol is literally \<^verbatim>\<open>\<^term>\<close>.) |
736 |
736 |
|
737 \<^item> @{system_option update_path_cartouches} to update file-system paths to |
|
738 use cartouches: this depends on language markup provided by semantic |
|
739 processing of parsed input. |
|
740 |
737 It is also possible to produce custom updates in Isabelle/ML, by reporting |
741 It is also possible to produce custom updates in Isabelle/ML, by reporting |
738 \<^ML>\<open>Markup.update\<close> with the precise source position and a replacement |
742 \<^ML>\<open>Markup.update\<close> with the precise source position and a replacement |
739 text. This operation should be made conditional on specific system options, |
743 text. This operation should be made conditional on specific system options, |
740 similar to the ones above. Searching the above option names in ML sources of |
744 similar to the ones above. Searching the above option names in ML sources of |
741 \<^dir>\<open>$ISABELLE_HOME/src/Pure\<close> provides some examples. |
745 \<^dir>\<open>$ISABELLE_HOME/src/Pure\<close> provides some examples. |