changeset 69599 caa7e406056d
parent 69593 3dda49e08b9d
child 69601 c51a9bd4cf09
equal deleted inserted replaced
69598:81caae4fc4fa 69599:caa7e406056d
   672   for such ambitious applications:
   672   for such ambitious applications:
   673   @{verbatim [display]
   673   @{verbatim [display]
   674 \<open>ISABELLE_TOOL_JAVA_OPTIONS="-Xms4g -Xmx32g -Xss16m"
   674 \<open>ISABELLE_TOOL_JAVA_OPTIONS="-Xms4g -Xmx32g -Xss16m"
   675 ML_OPTIONS="--minheap 4G --maxheap 32G"
   675 ML_OPTIONS="--minheap 4G --maxheap 32G"
   676 \<close>}
   676 \<close>}
   677 \<close>
   680 section \<open>Update theory sources based on PIDE markup \label{sec:tool-update}\<close>
   682 text \<open>
   683   The @{tool_def "update"} tool updates theory sources based on markup that is
   684   produced from a running PIDE session (similar to @{tool dump}
   685   \secref{sec:tool-dump}). Its command-line usage is: @{verbatim [display]
   686 \<open>Usage: isabelle update [OPTIONS] [SESSIONS ...]
   688   Options are:
   689     -B NAME      include session NAME and all descendants
   690     -D DIR       include session directory and select its sessions
   691     -R           operate on requirements of selected sessions
   692     -X NAME      exclude sessions from group NAME and all descendants
   693     -a           select all sessions
   694     -d DIR       include session directory
   695     -g NAME      select session group NAME
   696     -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
   697     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   698     -s           system build mode for logic image
   699     -u OPT       overide update option: shortcut for "-o update_OPT"
   700     -v           verbose
   701     -x NAME      exclude session NAME and all descendants
   703   Update theory sources based on PIDE markup.\<close>}
   705   \<^medskip> Options \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> and the
   706   remaining command-line arguments specify sessions as in @{tool build}
   707   (\secref{sec:tool-build}) or @{tool dump} (\secref{sec:tool-dump}).
   709   \<^medskip> Options \<^verbatim>\<open>-l\<close> and \<^verbatim>\<open>-s\<close> specify the underlying logic image is in @{tool
   710   dump} (\secref{sec:tool-dump}).
   712   \<^medskip> Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
   714   \<^medskip> Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
   715   (\secref{sec:tool-build}). Option \<^verbatim>\<open>-u\<close> refers to specific \<^verbatim>\<open>update\<close>
   716   options, by relying on naming convention: ``\<^verbatim>\<open>-u\<close>~\<open>OPT\<close>'' is a shortcut for
   717   ``\<^verbatim>\<open>-o\<close>~\<^verbatim>\<open>update_\<close>\<open>OPT\<close>''.
   719   \<^medskip> The following update options are supported:
   721     \<^item> @{system_option update_inner_syntax_cartouches} to update inner syntax
   722     (types, terms, etc.)~to use cartouches, instead of double-quoted strings
   723     or atomic identifiers. For example, ``\<^theory_text>\<open>lemma \<doublequote>x =
   724     x\<doublequote>\<close>'' is replaced by ``\<^theory_text>\<open>lemma \<open>x = x\<close>\<close>'', and ``\<^theory_text>\<open>fix x\<close>''
   725     is replaced by ``\<^theory_text>\<open>fix \<open>x\<close>\<close>''.
   727     \<^item> @{system_option update_mixfix_cartouches} to update mixfix templates to
   728     use cartouches instead of double-quoted strings. For example, ``\<^theory_text>\<open>(infixl
   729     \<doublequote>+\<doublequote> 65)\<close>'' is replaced by ``\<^theory_text>\<open>(infixl \<open>+\<close>
   730     65)\<close>''.
   732     \<^item> @{system_option update_control_cartouches} to update antiquotations to
   733     use the compact form with control symbol and cartouche argument. For
   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>.)
   737   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
   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
   741   \<^dir>\<open>$ISABELLE_HOME/src/Pure\<close> provides some examples.
   743   Different update options can be in conflict by producing overlapping edits:
   744   this may require to run @{tool update} multiple times, but it is often
   745   better to enable particular update options separately and commit the changes
   746   one-by-one.
   747 \<close>
   750 subsubsection \<open>Examples\<close>
   752 text \<open>
   753   Update some cartouche notation in all theory sources required for session
   754   \<^verbatim>\<open>HOL-Analysis\<close>:
   756   @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l Pure HOL-Analysis\<close>}
   758   \<^smallskip> Update the same for all application sessions based on \<^verbatim>\<open>HOL-Analysis\<close> ---
   759   its image is taken as starting point and its sources are not touched:
   761   @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l HOL-Analysis -B HOL-Analysis\<close>}
   763   \<^smallskip> This two-stage approach reduces resource requirements of the running PIDE
   764   session: a base image like \<^verbatim>\<open>HOL-Analysis\<close> (or \<^verbatim>\<open>HOL\<close>, \<^verbatim>\<open>HOL-Library\<close>) is
   765   more compact than importing all required theory (and ML) source files from
   766   \<^verbatim>\<open>Pure\<close>.
   768   \<^smallskip> Update sessions that build on \<^verbatim>\<open>HOL-Proofs\<close>, which need to be run
   769   separately with special options as follows:
   771   @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l HOL-Proofs -B HOL-Proofs
   772   -o record_proofs=2 -o parallel_proofs=0\<close>}
   774   \<^smallskip> See also the end of \secref{sec:tool-dump} for hints on increasing
   775   Isabelle/ML heap sizes for very big PIDE processes that include many
   776   sessions, notably from the Archive of Formal Proofs.
   678 \<close>
   777 \<close>
   680 end
   779 end