src/Doc/System/Interfaces.thy
author wenzelm
Fri May 17 19:04:52 2013 +0200 (2013-05-17)
changeset 52056 fc458f304f93
parent 51054 d6de6e81574d
child 52062 4f91262e7f33
permissions -rw-r--r--
added isabelle-process option -o;
     1 theory Interfaces
     2 imports Base
     3 begin
     4 
     5 chapter {* User interfaces *}
     6 
     7 section {* Isabelle/jEdit Prover IDE \label{sec:tool-jedit} *}
     8 
     9 text {* The @{tool_def jedit} tool invokes a version of
    10   jEdit\footnote{\url{http://www.jedit.org/}} that has been augmented
    11   with some plugins to provide a fully-featured Prover IDE:
    12 \begin{ttbox} Usage: isabelle jedit [OPTIONS]
    13   [FILES ...]
    14 
    15   Options are:
    16     -J OPTION    add JVM runtime option (default JEDIT_JAVA_OPTIONS)
    17     -b           build only
    18     -d DIR       include session directory
    19     -f           fresh build
    20     -j OPTION    add jEdit runtime option (default JEDIT_OPTIONS)
    21     -l NAME      logic image name (default ISABELLE_LOGIC)
    22     -m MODE      add print mode for output
    23     -n           no build dialog for session image on startup
    24     -s           system build mode for session image
    25 
    26 Start jEdit with Isabelle plugin setup and open theory FILES
    27 (default "\$USER_HOME/Scratch.thy").
    28 \end{ttbox}
    29 
    30   The @{verbatim "-l"} option specifies the session name of the logic
    31   image to be used for proof processing.  Additional session root
    32   directories may be included via option @{verbatim "-d"} to augment
    33   that name space (see also \secref{sec:tool-build}).
    34 
    35   By default, the specified image is checked and built on demand, see
    36   also @{tool build_dialog}.  The @{verbatim "-s"} determines where to
    37   store the result session image (see also \secref{sec:tool-build}).
    38   The @{verbatim "-n"} option bypasses the session build dialog.
    39 
    40   The @{verbatim "-m"} option specifies additional print modes for the
    41   prover process.
    42 
    43   The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass
    44   additional low-level options to the JVM or jEdit, respectively.  The
    45   defaults are provided by the Isabelle settings environment
    46   (\secref{sec:settings}).
    47 
    48   The @{verbatim "-b"} and @{verbatim "-f"} options control the
    49   self-build mechanism of Isabelle/jEdit.  This is only relevant for
    50   building from sources, which also requires an auxiliary @{verbatim
    51   jedit_build}
    52   component.\footnote{\url{http://isabelle.in.tum.de/components}} Note
    53   that official Isabelle releases already include a version of
    54   Isabelle/jEdit that is built properly.
    55 *}
    56 
    57 
    58 section {* Proof General / Emacs *}
    59 
    60 text {* The @{tool_def emacs} tool invokes a version of Emacs and
    61   Proof General\footnote{http://proofgeneral.inf.ed.ac.uk/} within the
    62   regular Isabelle settings environment (\secref{sec:settings}).  This
    63   is more convenient than starting Emacs separately, loading the Proof
    64   General LISP files, and then attempting to start Isabelle with
    65   dynamic @{setting PATH} lookup etc., although it might fail if a
    66   different version of Proof General is already part of the Emacs
    67   installation of the operating system.
    68 
    69   The actual interface script is part of the Proof General
    70   distribution; its usage depends on the particular version.  There
    71   are some options available, such as @{verbatim "-l"} for passing the
    72   logic image to be used by default, or @{verbatim "-m"} to tune the
    73   standard print mode of the prover process.  The following Isabelle
    74   settings are particularly important for Proof General:
    75 
    76   \begin{description}
    77 
    78   \item[@{setting_def PROOFGENERAL_HOME}] points to the main
    79   installation directory of the Proof General distribution.  This is
    80   implicitly provided for versions of Proof General that are
    81   distributed as Isabelle component, see also \secref{sec:components};
    82   otherwise it needs to be configured manually.
    83 
    84   \item[@{setting_def PROOFGENERAL_OPTIONS}] is implicitly prefixed to
    85   the command line of any invocation of the Proof General @{verbatim
    86   interface} script.  This allows to provide persistent default
    87   options for the invocation of \texttt{isabelle emacs}.
    88 
    89   \end{description}
    90 *}
    91 
    92 
    93 section {* Plain TTY interaction \label{sec:tool-tty} *}
    94 
    95 text {*
    96   The @{tool_def tty} tool runs the Isabelle process interactively
    97   within a plain terminal session:
    98 \begin{ttbox}
    99 Usage: isabelle tty [OPTIONS]
   100 
   101   Options are:
   102     -l NAME      logic image name (default ISABELLE_LOGIC)
   103     -m MODE      add print mode for output
   104     -p NAME      line editor program name (default ISABELLE_LINE_EDITOR)
   105 
   106   Run Isabelle process with plain tty interaction and line editor.
   107 \end{ttbox}
   108 
   109   The @{verbatim "-l"} option specifies the logic image.  The
   110   @{verbatim "-m"} option specifies additional print modes.  The
   111   @{verbatim "-p"} option specifies an alternative line editor (such
   112   as the @{executable_def rlwrap} wrapper for GNU readline); the
   113   fall-back is to use raw standard input.
   114 
   115   Regular interaction works via the standard Isabelle/Isar toplevel
   116   loop.  The Isar command @{command exit} drops out into the
   117   bare-bones ML system, which is occasionally useful for debugging of
   118   the Isar infrastructure itself.  Invoking @{ML Isar.loop}~@{verbatim
   119   "();"} in ML will return to the Isar toplevel.  *}
   120 
   121 
   122 
   123 section {* Theory graph browser \label{sec:browse} *}
   124 
   125 text {* The Isabelle graph browser is a general tool for visualizing
   126   dependency graphs.  Certain nodes of the graph (i.e.\ theories) can
   127   be grouped together in ``directories'', whose contents may be
   128   hidden, thus enabling the user to collapse irrelevant portions of
   129   information.  The browser is written in Java, it can be used both as
   130   a stand-alone application and as an applet.  *}
   131 
   132 
   133 subsection {* Invoking the graph browser *}
   134 
   135 text {* The stand-alone version of the graph browser is wrapped up as
   136   @{tool_def browser}:
   137 \begin{ttbox}
   138 Usage: isabelle browser [OPTIONS] [GRAPHFILE]
   139 
   140   Options are:
   141     -b           Admin/build only
   142     -c           cleanup -- remove GRAPHFILE after use
   143     -o FILE      output to FILE (ps, eps, pdf)
   144 \end{ttbox}
   145   When no filename is specified, the browser automatically changes to
   146   the directory @{setting ISABELLE_BROWSER_INFO}.
   147 
   148   \medskip The @{verbatim "-b"} option indicates that this is for
   149   administrative build only, i.e.\ no browser popup if no files are
   150   given.
   151 
   152   The @{verbatim "-c"} option causes the input file to be removed
   153   after use.
   154 
   155   The @{verbatim "-o"} option indicates batch-mode operation, with the
   156   output written to the indicated file; note that @{verbatim pdf}
   157   produces an @{verbatim eps} copy as well.
   158 
   159   \medskip The applet version of the browser is part of the standard
   160   WWW theory presentation, see the link ``theory dependencies'' within
   161   each session index.
   162 *}
   163 
   164 
   165 subsection {* Using the graph browser *}
   166 
   167 text {*
   168   The browser's main window, which is shown in
   169   \figref{fig:browserwindow}, consists of two sub-windows.  In the
   170   left sub-window, the directory tree is displayed. The graph itself
   171   is displayed in the right sub-window.
   172 
   173   \begin{figure}[ht]
   174   \includegraphics[width=\textwidth]{browser_screenshot}
   175   \caption{\label{fig:browserwindow} Browser main window}
   176   \end{figure}
   177 *}
   178 
   179 
   180 subsubsection {* The directory tree window *}
   181 
   182 text {*
   183   We describe the usage of the directory browser and the meaning of
   184   the different items in the browser window.
   185 
   186   \begin{itemize}
   187 
   188   \item A red arrow before a directory name indicates that the
   189   directory is currently ``folded'', i.e.~the nodes in this directory
   190   are collapsed to one single node. In the right sub-window, the names
   191   of nodes corresponding to folded directories are enclosed in square
   192   brackets and displayed in red color.
   193 
   194   \item A green downward arrow before a directory name indicates that
   195   the directory is currently ``unfolded''. It can be folded by
   196   clicking on the directory name.  Clicking on the name for a second
   197   time unfolds the directory again.  Alternatively, a directory can
   198   also be unfolded by clicking on the corresponding node in the right
   199   sub-window.
   200 
   201   \item Blue arrows stand before ordinary node names. When clicking on
   202   such a name (i.e.\ that of a theory), the graph display window
   203   focuses to the corresponding node. Double clicking invokes a text
   204   viewer window in which the contents of the theory file are
   205   displayed.
   206 
   207   \end{itemize}
   208 *}
   209 
   210 
   211 subsubsection {* The graph display window *}
   212 
   213 text {*
   214   When pointing on an ordinary node, an upward and a downward arrow is
   215   shown.  Initially, both of these arrows are green. Clicking on the
   216   upward or downward arrow collapses all predecessor or successor
   217   nodes, respectively. The arrow's color then changes to red,
   218   indicating that the predecessor or successor nodes are currently
   219   collapsed. The node corresponding to the collapsed nodes has the
   220   name ``@{verbatim "[....]"}''. To uncollapse the nodes again, simply
   221   click on the red arrow or on the node with the name ``@{verbatim
   222   "[....]"}''. Similar to the directory browser, the contents of
   223   theory files can be displayed by double clicking on the
   224   corresponding node.
   225 *}
   226 
   227 
   228 subsubsection {* The ``File'' menu *}
   229 
   230 text {*
   231   Due to Java Applet security restrictions this menu is only available
   232   in the full application version. The meaning of the menu items is as
   233   follows:
   234 
   235   \begin{description}
   236 
   237   \item[Open \dots] Open a new graph file.
   238 
   239   \item[Export to PostScript] Outputs the current graph in Postscript
   240   format, appropriately scaled to fit on one single sheet of A4 paper.
   241   The resulting file can be printed directly.
   242 
   243   \item[Export to EPS] Outputs the current graph in Encapsulated
   244   Postscript format. The resulting file can be included in other
   245   documents.
   246 
   247   \item[Quit] Quit the graph browser.
   248 
   249   \end{description}
   250 *}
   251 
   252 
   253 subsection {* Syntax of graph definition files *}
   254 
   255 text {*
   256   A graph definition file has the following syntax:
   257 
   258   \begin{center}\small
   259   \begin{tabular}{rcl}
   260     @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}+"} \\
   261     @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }*"}
   262   \end{tabular}
   263   \end{center}
   264 
   265   The meaning of the items in a vertex description is as follows:
   266 
   267   \begin{description}
   268 
   269   \item[@{text vertex_name}] The name of the vertex.
   270 
   271   \item[@{text vertex_ID}] The vertex identifier. Note that there may
   272   be several vertices with equal names, whereas identifiers must be
   273   unique.
   274 
   275   \item[@{text dir_name}] The name of the ``directory'' the vertex
   276   should be placed in.  A ``@{verbatim "+"}'' sign after @{text
   277   dir_name} indicates that the nodes in the directory are initially
   278   visible. Directories are initially invisible by default.
   279 
   280   \item[@{text path}] The path of the corresponding theory file. This
   281   is specified relatively to the path of the graph definition file.
   282 
   283   \item[List of successor/predecessor nodes] A ``@{verbatim "<"}''
   284   sign before the list means that successor nodes are listed, a
   285   ``@{verbatim ">"}'' sign means that predecessor nodes are listed. If
   286   neither ``@{verbatim "<"}'' nor ``@{verbatim ">"}'' is found, the
   287   browser assumes that successor nodes are listed.
   288 
   289   \end{description}
   290 *}
   291 
   292 end