doc-src/System/Thy/document/Interfaces.tex
author wenzelm
Sat Apr 28 17:50:42 2012 +0200 (2012-04-28)
changeset 47825 4f25960417ae
parent 47824 65082431af2a
child 47826 7c97bfe3a501
permissions -rw-r--r--
some coverage of Isabelle/Scala tools;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Interfaces}%
     4 %
     5 \isadelimtheory
     6 %
     7 \endisadelimtheory
     8 %
     9 \isatagtheory
    10 \isacommand{theory}\isamarkupfalse%
    11 \ Interfaces\isanewline
    12 \isakeyword{imports}\ Base\isanewline
    13 \isakeyword{begin}%
    14 \endisatagtheory
    15 {\isafoldtheory}%
    16 %
    17 \isadelimtheory
    18 %
    19 \endisadelimtheory
    20 %
    21 \isamarkupchapter{User interfaces%
    22 }
    23 \isamarkuptrue%
    24 %
    25 \isamarkupsection{Plain TTY interaction \label{sec:tool-tty}%
    26 }
    27 \isamarkuptrue%
    28 %
    29 \begin{isamarkuptext}%
    30 The \indexdef{}{tool}{tty}\hypertarget{tool.tty}{\hyperlink{tool.tty}{\mbox{\isa{\isatt{tty}}}}} tool runs the Isabelle process interactively
    31   within a plain terminal session:
    32 \begin{ttbox}
    33 Usage: tty [OPTIONS]
    34 
    35   Options are:
    36     -l NAME      logic image name (default ISABELLE_LOGIC)
    37     -m MODE      add print mode for output
    38     -p NAME      line editor program name (default ISABELLE_LINE_EDITOR)
    39 
    40   Run Isabelle process with plain tty interaction, and optional line editor.
    41 \end{ttbox}
    42 
    43   The \verb|-l| option specifies the logic image.  The
    44   \verb|-m| option specifies additional print modes.  The
    45   \verb|-p| option specifies an alternative line editor (such
    46   as the \indexdef{}{executable}{rlwrap}\hypertarget{executable.rlwrap}{\hyperlink{executable.rlwrap}{\mbox{\isa{\isatt{rlwrap}}}}} wrapper for GNU readline); the
    47   fall-back is to use raw standard input.
    48 
    49   Regular interaction is via the standard Isabelle/Isar toplevel loop.
    50   The Isar command \hyperlink{command.exit}{\mbox{\isa{\isacommand{exit}}}} drops out into the raw ML system,
    51   which is occasionally useful for low-level debugging.  Invoking \verb|Isar.loop|~\verb|();| in ML will return to the Isar toplevel.%
    52 \end{isamarkuptext}%
    53 \isamarkuptrue%
    54 %
    55 \isamarkupsection{Proof General / Emacs%
    56 }
    57 \isamarkuptrue%
    58 %
    59 \begin{isamarkuptext}%
    60 The \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatt{emacs}}}}} tool invokes a version of Emacs and Proof
    61   General within the regular Isabelle settings environment
    62   (\secref{sec:settings}).  This is more robust than starting Emacs
    63   separately, loading the Proof General lisp files, and then
    64   attempting to start Isabelle with dynamic \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}} lookup
    65   etc.
    66 
    67   The actual interface script is part of the Proof General
    68   distribution~\cite{proofgeneral}; its usage depends on the
    69   particular version.  There are some options available, such as
    70   \verb|-l| for passing the logic image to be used by default,
    71   or \verb|-m| to tune the standard print mode.  The following
    72   Isabelle settings are particularly important for Proof General:
    73 
    74   \begin{description}
    75 
    76   \item[\indexdef{}{setting}{PROOFGENERAL\_HOME}\hypertarget{setting.PROOFGENERAL-HOME}{\hyperlink{setting.PROOFGENERAL-HOME}{\mbox{\isa{\isatt{PROOFGENERAL{\isaliteral{5F}{\isacharunderscore}}HOME}}}}}] points to the main
    77   installation directory of the Proof General distribution.  The
    78   default settings try to locate this in a number of standard places,
    79   notably \verb|$ISABELLE_HOME/contrib/ProofGeneral|.
    80 
    81   \item[\indexdef{}{setting}{PROOFGENERAL\_OPTIONS}\hypertarget{setting.PROOFGENERAL-OPTIONS}{\hyperlink{setting.PROOFGENERAL-OPTIONS}{\mbox{\isa{\isatt{PROOFGENERAL{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}}}] is implicitly prefixed to
    82   the command line of any invocation of the Proof General \verb|interface| script.
    83 
    84   \item[\indexdef{}{setting}{XSYMBOL\_INSTALLFONTS}\hypertarget{setting.XSYMBOL-INSTALLFONTS}{\hyperlink{setting.XSYMBOL-INSTALLFONTS}{\mbox{\isa{\isatt{XSYMBOL{\isaliteral{5F}{\isacharunderscore}}INSTALLFONTS}}}}}] may contain a small shell
    85   script to install the X11 fonts required for the old X-Symbols mode
    86   of Proof General.  This is only relevant if the X11 display server
    87   runs on a different machine than the Emacs application, with a
    88   different file-system view on the Proof General installation.  Under
    89   most circumstances Proof General 3.x is able to refer to the font
    90   files that are part of its distribution, and Proof General 4.x finds
    91   its fonts by different means.
    92 
    93   \end{description}%
    94 \end{isamarkuptext}%
    95 \isamarkuptrue%
    96 %
    97 \isamarkupsection{Isabelle/jEdit Prover IDE \label{sec:tool-jedit}%
    98 }
    99 \isamarkuptrue%
   100 %
   101 \begin{isamarkuptext}%
   102 The \indexdef{}{tool}{jedit}\hypertarget{tool.jedit}{\hyperlink{tool.jedit}{\mbox{\isa{\isatt{jedit}}}}} tool invokes a version of jEdit that has
   103   been augmented with some components to provide a fully-featured
   104   Prover IDE (based on Isabelle/Scala):
   105 \begin{ttbox}
   106 Usage: isabelle jedit [OPTIONS] [FILES ...]
   107 
   108   Options are:
   109     -J OPTION    add JVM runtime option (default JEDIT_JAVA_OPTIONS)
   110     -b           build only
   111     -d           enable debugger
   112     -f           fresh build
   113     -j OPTION    add jEdit runtime option (default JEDIT_OPTIONS)
   114     -l NAME      logic image name (default ISABELLE_LOGIC)
   115     -m MODE      add print mode for output
   116 
   117 Start jEdit with Isabelle plugin setup and opens theory FILES
   118 (default Scratch.thy).
   119 \end{ttbox}
   120 
   121 The \verb|-J| and \verb|-j| options allow to pass
   122 additional low-level options to the JVM or jEdit, respectively.  The
   123 defaults are provided by the Isabelle settings environment.
   124 
   125 The \verb|-d| option allows to connect to the runtime debugger
   126 of the JVM.  Note that the Scala Console of Isabelle/jEdit is more
   127 convenient in most practical situations.
   128 
   129 The \verb|-b| and \verb|-f| options control the
   130 self-build mechanism of Isabelle/jEdit.  This is only relevant for
   131 building from sources, which also requires an auxiliary \verb|jedit_build| component.  Official Isabelle releases already include a
   132 version of Isabelle/jEdit that is built properly.
   133 
   134 The \verb|-l| option specifies the logic image.  The
   135 \verb|-m| option specifies additional print modes.%
   136 \end{isamarkuptext}%
   137 \isamarkuptrue%
   138 %
   139 \isadelimtheory
   140 %
   141 \endisadelimtheory
   142 %
   143 \isatagtheory
   144 \isacommand{end}\isamarkupfalse%
   145 %
   146 \endisatagtheory
   147 {\isafoldtheory}%
   148 %
   149 \isadelimtheory
   150 %
   151 \endisadelimtheory
   152 \end{isabellebody}%
   153 %%% Local Variables:
   154 %%% mode: latex
   155 %%% TeX-master: "root"
   156 %%% End: