equal
deleted
inserted
replaced
738 \<^ML>\<open>Markup.update\<close> with the precise source position and a replacement |
738 \<^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, |
739 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 |
740 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. |
741 \<^dir>\<open>$ISABELLE_HOME/src/Pure\<close> provides some examples. |
742 |
742 |
743 Different update options can be in conflict by producing overlapping edits: |
743 Updates can be in conflict by producing nested or overlapping edits: this |
744 this may require to run @{tool update} multiple times, but it is often |
744 may require to run @{tool update} multiple times. |
745 better to enable particular update options separately and commit the changes |
|
746 one-by-one. |
|
747 \<close> |
745 \<close> |
748 |
746 |
749 |
747 |
750 subsubsection \<open>Examples\<close> |
748 subsubsection \<open>Examples\<close> |
751 |
749 |