wenzelm@28224: theory Misc
wenzelm@43564: imports Base
wenzelm@28224: begin
wenzelm@28224: 
wenzelm@28224: chapter {* Miscellaneous tools \label{ch:tools} *}
wenzelm@28224: 
wenzelm@28224: text {*
wenzelm@28224:   Subsequently we describe various Isabelle related utilities, given
wenzelm@28224:   in alphabetical order.
wenzelm@28224: *}
wenzelm@28224: 
wenzelm@28224: 
wenzelm@48844: section {* Resolving Isabelle components \label{sec:tool-components} *}
wenzelm@48844: 
wenzelm@48844: text {*
wenzelm@48844:   The @{tool_def components} tool resolves Isabelle components:
wenzelm@48844: \begin{ttbox}
wenzelm@48844: Usage: isabelle components [OPTIONS] [COMPONENTS ...]
wenzelm@48844: 
wenzelm@48844:   Options are:
wenzelm@50653:     -I           init user settings
wenzelm@48844:     -R URL       component repository
wenzelm@48844:                  (default $ISABELLE_COMPONENT_REPOSITORY)
wenzelm@48844:     -a           all missing components
wenzelm@48844:     -l           list status
wenzelm@48844: 
wenzelm@48844:   Resolve Isabelle components via download and installation.
wenzelm@48844:   COMPONENTS are identified via base name.
wenzelm@48844: 
wenzelm@48844:   ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"
wenzelm@48844: \end{ttbox}
wenzelm@48844: 
wenzelm@48844:   Components are initialized as described in \secref{sec:components}
wenzelm@48844:   in a permissive manner, which can mark components as ``missing''.
wenzelm@48844:   This state is amended by letting @{tool "components"} download and
wenzelm@48844:   unpack components that are published on the default component
wenzelm@48844:   repository \url{http://isabelle.in.tum.de/components/} in
wenzelm@48844:   particular.
wenzelm@48844: 
wenzelm@48844:   Option @{verbatim "-R"} specifies an alternative component
wenzelm@48844:   repository.  Note that @{verbatim "file:///"} URLs can be used for
wenzelm@48844:   local directories.
wenzelm@48844: 
wenzelm@48844:   Option @{verbatim "-a"} selects all missing components to be
wenzelm@48844:   installed.  Explicit components may be named as command
wenzelm@48844:   line-arguments as well.  Note that components are uniquely
wenzelm@48844:   identified by their base name, while the installation takes place in
wenzelm@48844:   the location that was specified in the attempt to initialize the
wenzelm@48844:   component before.
wenzelm@48844: 
wenzelm@48844:   Option @{verbatim "-l"} lists the current state of available and
wenzelm@48844:   missing components with their location (full name) within the
wenzelm@50653:   file-system.
wenzelm@50653: 
wenzelm@50653:   Option @{verbatim "-I"} initializes the user settings file to
wenzelm@50653:   subscribe to the standard components specified in the Isabelle
wenzelm@50653:   repository clone --- this does not make any sense for regular
wenzelm@50653:   Isabelle releases.  If the file already exists, it needs to be
wenzelm@50653:   edited manually according to the printed explanation.
wenzelm@50653: *}
wenzelm@48844: 
wenzelm@48844: 
wenzelm@28224: section {* Displaying documents *}
wenzelm@28224: 
wenzelm@48602: text {* The @{tool_def display} tool displays documents in DVI or PDF
wenzelm@28224:   format:
wenzelm@28224: \begin{ttbox}
wenzelm@48602: Usage: isabelle display [OPTIONS] FILE
wenzelm@28224: 
wenzelm@28224:   Options are:
wenzelm@28224:     -c           cleanup -- remove FILE after use
wenzelm@28224: 
wenzelm@28224:   Display document FILE (in DVI format).
wenzelm@28224: \end{ttbox}
wenzelm@28224: 
wenzelm@28224:   \medskip The @{verbatim "-c"} option causes the input file to be
wenzelm@28224:   removed after use.  The program for viewing @{verbatim dvi} files is
wenzelm@28224:   determined by the @{setting DVI_VIEWER} setting.
wenzelm@28224: *}
wenzelm@28224: 
wenzelm@28224: 
wenzelm@28224: section {* Viewing documentation \label{sec:tool-doc} *}
wenzelm@28224: 
wenzelm@28224: text {*
wenzelm@48602:   The @{tool_def doc} tool displays online documentation:
wenzelm@28224: \begin{ttbox}
wenzelm@48602: Usage: isabelle doc [DOC]
wenzelm@28224: 
wenzelm@28224:   View Isabelle documentation DOC, or show list of available documents.
wenzelm@28224: \end{ttbox}
wenzelm@28224:   If called without arguments, it lists all available documents. Each
wenzelm@28224:   line starts with an identifier, followed by a short description. Any
wenzelm@28224:   of these identifiers may be specified as the first argument in order
wenzelm@28224:   to have the corresponding document displayed.
wenzelm@28224: 
wenzelm@28224:   \medskip The @{setting ISABELLE_DOCS} setting specifies the list of
wenzelm@28224:   directories (separated by colons) to be scanned for documentations.
wenzelm@28224:   The program for viewing @{verbatim dvi} files is determined by the
wenzelm@28224:   @{setting DVI_VIEWER} setting.
wenzelm@28224: *}
wenzelm@28224: 
wenzelm@28224: 
wenzelm@47828: section {* Shell commands within the settings environment \label{sec:tool-env} *}
wenzelm@47828: 
wenzelm@48602: text {* The @{tool_def env} tool is a direct wrapper for the standard
wenzelm@48602:   @{verbatim "/usr/bin/env"} command on POSIX systems, running within
wenzelm@48602:   the Isabelle settings environment (\secref{sec:settings}).
wenzelm@47828: 
wenzelm@47828:   The command-line arguments are that of the underlying version of
wenzelm@47828:   @{verbatim env}.  For example, the following invokes an instance of
wenzelm@47828:   the GNU Bash shell within the Isabelle environment:
wenzelm@47828: \begin{alltt}
wenzelm@47828:   isabelle env bash
wenzelm@47828: \end{alltt}
wenzelm@47828: *}
wenzelm@47828: 
wenzelm@47828: 
wenzelm@28224: section {* Getting logic images *}
wenzelm@28224: 
wenzelm@48602: text {* The @{tool_def findlogics} tool traverses all directories
wenzelm@28224:   specified in @{setting ISABELLE_PATH}, looking for Isabelle logic
wenzelm@28224:   images. Its usage is:
wenzelm@28224: \begin{ttbox}
wenzelm@48577: Usage: isabelle findlogics
wenzelm@28224: 
wenzelm@28224:   Collect heap file names from ISABELLE_PATH.
wenzelm@28224: \end{ttbox}
wenzelm@28224: 
wenzelm@28224:   The base names of all files found on the path are printed --- sorted
wenzelm@28224:   and with duplicates removed. Also note that lookup in @{setting
wenzelm@28224:   ISABELLE_PATH} includes the current values of @{setting ML_SYSTEM}
wenzelm@28224:   and @{setting ML_PLATFORM}. Thus switching to another ML compiler
wenzelm@28224:   may change the set of logic images available.
wenzelm@28224: *}
wenzelm@28224: 
wenzelm@28224: 
wenzelm@28224: section {* Inspecting the settings environment \label{sec:tool-getenv} *}
wenzelm@28224: 
wenzelm@48602: text {* The Isabelle settings environment --- as provided by the
wenzelm@28224:   site-default and user-specific settings files --- can be inspected
wenzelm@48602:   with the @{tool_def getenv} tool:
wenzelm@28224: \begin{ttbox}
wenzelm@48602: Usage: isabelle getenv [OPTIONS] [VARNAMES ...]
wenzelm@28224: 
wenzelm@28224:   Options are:
wenzelm@28224:     -a           display complete environment
wenzelm@28224:     -b           print values only (doesn't work for -a)
wenzelm@31497:     -d FILE      dump complete environment to FILE
wenzelm@31497:                  (null terminated entries)
wenzelm@28224: 
wenzelm@28224:   Get value of VARNAMES from the Isabelle settings.
wenzelm@28224: \end{ttbox}
wenzelm@28224: 
wenzelm@28224:   With the @{verbatim "-a"} option, one may inspect the full process
wenzelm@28224:   environment that Isabelle related programs are run in. This usually
wenzelm@28224:   contains much more variables than are actually Isabelle settings.
wenzelm@28224:   Normally, output is a list of lines of the form @{text
wenzelm@28224:   name}@{verbatim "="}@{text value}. The @{verbatim "-b"} option
wenzelm@28224:   causes only the values to be printed.
wenzelm@31497: 
wenzelm@31497:   Option @{verbatim "-d"} produces a dump of the complete environment
wenzelm@31497:   to the specified file.  Entries are terminated by the ASCII null
wenzelm@31497:   character, i.e.\ the C string terminator.
wenzelm@28224: *}
wenzelm@28224: 
wenzelm@28224: 
wenzelm@28224: subsubsection {* Examples *}
wenzelm@28224: 
wenzelm@48815: text {* Get the location of @{setting ISABELLE_HOME_USER} where
wenzelm@48815:   user-specific information is stored:
wenzelm@28224: \begin{ttbox}
wenzelm@48815: isabelle getenv ISABELLE_HOME_USER
wenzelm@28224: \end{ttbox}
wenzelm@28224: 
wenzelm@48815:   \medskip Get the value only of the same settings variable, which is
wenzelm@48815: particularly useful in shell scripts:
wenzelm@28224: \begin{ttbox}
wenzelm@28504: isabelle getenv -b ISABELLE_OUTPUT
wenzelm@28224: \end{ttbox}
wenzelm@28224: *}
wenzelm@28224: 
wenzelm@28224: 
wenzelm@28224: section {* Installing standalone Isabelle executables \label{sec:tool-install} *}
wenzelm@28224: 
wenzelm@48602: text {* By default, the main Isabelle binaries (@{executable
wenzelm@48602:   "isabelle"} etc.)  are just run from their location within the
wenzelm@48602:   distribution directory, probably indirectly by the shell through its
wenzelm@48602:   @{setting PATH}.  Other schemes of installation are supported by the
wenzelm@48602:   @{tool_def install} tool:
wenzelm@28224: \begin{ttbox}
wenzelm@50132: Usage: isabelle install [OPTIONS] BINDIR
wenzelm@28224: 
wenzelm@28224:   Options are:
wenzelm@50132:     -d DISTDIR   refer to DISTDIR as Isabelle distribution
wenzelm@28224:                  (default ISABELLE_HOME)
wenzelm@28224: 
wenzelm@50132:   Install Isabelle executables with absolute references to the
wenzelm@28224:   distribution directory.
wenzelm@28224: \end{ttbox}
wenzelm@28224: 
wenzelm@28224:   The @{verbatim "-d"} option overrides the current Isabelle
wenzelm@28224:   distribution directory as determined by @{setting ISABELLE_HOME}.
wenzelm@28224: 
wenzelm@50132:   The @{text BINDIR} argument tells where executable wrapper scripts
wenzelm@50132:   for @{executable "isabelle-process"} and @{executable isabelle}
wenzelm@50132:   should be placed, which is typically a directory in the shell's
wenzelm@50132:   @{setting PATH}, such as @{verbatim "$HOME/bin"}.
wenzelm@48815: 
wenzelm@50132:   \medskip It is also possible to make symbolic links of the main
wenzelm@50132:   Isabelle executables manually, but making separate copies outside
wenzelm@50132:   the Isabelle distribution directory will not work!  *}
wenzelm@28224: 
wenzelm@28224: 
wenzelm@28224: section {* Creating instances of the Isabelle logo *}
wenzelm@28224: 
wenzelm@49072: text {* The @{tool_def logo} tool creates instances of the generic
wenzelm@49072:   Isabelle logo as EPS and PDF, for inclusion in {\LaTeX} documents.
wenzelm@28224: \begin{ttbox}
wenzelm@49072: Usage: isabelle logo [OPTIONS] XYZ
wenzelm@28224: 
wenzelm@49072:   Create instance XYZ of the Isabelle logo (as EPS and PDF).
wenzelm@28224: 
wenzelm@28224:   Options are:
wenzelm@49072:     -n NAME      alternative output base name (default "isabelle_xyx")
wenzelm@28224:     -q           quiet mode
wenzelm@28224: \end{ttbox}
wenzelm@48936: 
wenzelm@49072:   Option @{verbatim "-n"} specifies an altenative (base) name for the
wenzelm@49072:   generated files.  The default is @{verbatim "isabelle_"}@{text xyz}
wenzelm@49072:   in lower-case.
wenzelm@48936: 
wenzelm@48936:   Option @{verbatim "-q"} omits printing of the result file name.
wenzelm@48936: 
wenzelm@48936:   \medskip Implementors of Isabelle tools and applications are
wenzelm@48936:   encouraged to make derived Isabelle logos for their own projects
wenzelm@48936:   using this template.  *}
wenzelm@28224: 
wenzelm@28224: 
wenzelm@28224: section {* Printing documents *}
wenzelm@28224: 
wenzelm@28224: text {*
wenzelm@48602:   The @{tool_def print} tool prints documents:
wenzelm@28224: \begin{ttbox}
wenzelm@48602: Usage: isabelle print [OPTIONS] FILE
wenzelm@28224: 
wenzelm@28224:   Options are:
wenzelm@28224:     -c           cleanup -- remove FILE after use
wenzelm@28224: 
wenzelm@28224:   Print document FILE.
wenzelm@28224: \end{ttbox}
wenzelm@28224: 
wenzelm@28224:   The @{verbatim "-c"} option causes the input file to be removed
wenzelm@28224:   after use.  The printer spool command is determined by the @{setting
wenzelm@28224:   PRINT_COMMAND} setting.
wenzelm@28224: *}
wenzelm@28224: 
wenzelm@28224: 
wenzelm@28224: section {* Remove awkward symbol names from theory sources *}
wenzelm@28224: 
wenzelm@28224: text {*
wenzelm@48602:   The @{tool_def unsymbolize} tool tunes Isabelle theory sources to
wenzelm@28224:   improve readability for plain ASCII output (e.g.\ in email
wenzelm@28224:   communication).  Most notably, @{tool unsymbolize} replaces awkward
wenzelm@28224:   arrow symbols such as @{verbatim "\\"}@{verbatim "<Longrightarrow>"}
wenzelm@28224:   by @{verbatim "==>"}.
wenzelm@28224: \begin{ttbox}
wenzelm@48602: Usage: isabelle unsymbolize [FILES|DIRS...]
wenzelm@28224: 
wenzelm@28224:   Recursively find .thy/.ML files, removing unreadable symbol names.
wenzelm@28224:   Note: this is an ad-hoc script; there is no systematic way to replace
wenzelm@28224:   symbols independently of the inner syntax of a theory!
wenzelm@28224: 
wenzelm@28224:   Renames old versions of FILES by appending "~~".
wenzelm@28224: \end{ttbox}
wenzelm@28224: *}
wenzelm@28224: 
wenzelm@28224: 
wenzelm@28224: section {* Output the version identifier of the Isabelle distribution *}
wenzelm@28224: 
wenzelm@28224: text {*
wenzelm@48602:   The @{tool_def version} tool displays Isabelle version information:
wenzelm@41511: \begin{ttbox}
wenzelm@41511: Usage: isabelle version [OPTIONS]
wenzelm@41511: 
wenzelm@41511:   Options are:
wenzelm@41511:     -i           short identification (derived from Mercurial id)
wenzelm@41511: 
wenzelm@41511:   Display Isabelle version information.
wenzelm@41511: \end{ttbox}
wenzelm@41511: 
wenzelm@41511:   \medskip The default is to output the full version string of the
wenzelm@47827:   Isabelle distribution, e.g.\ ``@{verbatim "Isabelle2012: May 2012"}.
wenzelm@41511: 
wenzelm@41511:   The @{verbatim "-i"} option produces a short identification derived
wenzelm@41511:   from the Mercurial id of the @{setting ISABELLE_HOME} directory.
wenzelm@28224: *}
wenzelm@28224: 
wenzelm@28224: 
wenzelm@28224: section {* Convert XML to YXML *}
wenzelm@28224: 
wenzelm@28224: text {*
wenzelm@28224:   The @{tool_def yxml} tool converts a standard XML document (stdin)
wenzelm@28224:   to the much simpler and more efficient YXML format of Isabelle
wenzelm@28224:   (stdout).  The YXML format is defined as follows.
wenzelm@28224: 
wenzelm@28224:   \begin{enumerate}
wenzelm@28224: 
wenzelm@28224:   \item The encoding is always UTF-8.
wenzelm@28224: 
wenzelm@28224:   \item Body text is represented verbatim (no escaping, no special
wenzelm@28224:   treatment of white space, no named entities, no CDATA chunks, no
wenzelm@28224:   comments).
wenzelm@28224: 
wenzelm@28224:   \item Markup elements are represented via ASCII control characters
wenzelm@28224:   @{text "\<^bold>X = 5"} and @{text "\<^bold>Y = 6"} as follows:
wenzelm@28224: 
wenzelm@28224:   \begin{tabular}{ll}
wenzelm@28224:     XML & YXML \\\hline
wenzelm@28224:     @{verbatim "<"}@{text "name attribute"}@{verbatim "="}@{text "value \<dots>"}@{verbatim ">"} &
wenzelm@28224:     @{text "\<^bold>X\<^bold>Yname\<^bold>Yattribute"}@{verbatim "="}@{text "value\<dots>\<^bold>X"} \\
wenzelm@28224:     @{verbatim "</"}@{text name}@{verbatim ">"} & @{text "\<^bold>X\<^bold>Y\<^bold>X"} \\
wenzelm@28224:   \end{tabular}
wenzelm@28224: 
wenzelm@28224:   There is no special case for empty body text, i.e.\ @{verbatim
wenzelm@28224:   "<foo/>"} is treated like @{verbatim "<foo></foo>"}.  Also note that
wenzelm@28224:   @{text "\<^bold>X"} and @{text "\<^bold>Y"} may never occur in
wenzelm@28224:   well-formed XML documents.
wenzelm@28224: 
wenzelm@28224:   \end{enumerate}
wenzelm@28224: 
wenzelm@28224:   Parsing YXML is pretty straight-forward: split the text into chunks
wenzelm@28224:   separated by @{text "\<^bold>X"}, then split each chunk into
wenzelm@28224:   sub-chunks separated by @{text "\<^bold>Y"}.  Markup chunks start
wenzelm@28224:   with an empty sub-chunk, and a second empty sub-chunk indicates
wenzelm@28224:   close of an element.  Any other non-empty chunk consists of plain
wenzelm@44799:   text.  For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or
wenzelm@44799:   @{file "~~/src/Pure/PIDE/yxml.scala"}.
wenzelm@28224: 
wenzelm@28224:   YXML documents may be detected quickly by checking that the first
wenzelm@28224:   two characters are @{text "\<^bold>X\<^bold>Y"}.
wenzelm@28224: *}
wenzelm@28224: 
wenzelm@28224: end