src/Doc/System/Sessions.thy
changeset 69602 48e973251070
parent 69601 c51a9bd4cf09
child 69603 67ae2e164c0f
equal deleted inserted replaced
69601:c51a9bd4cf09 69602:48e973251070
   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