1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/System/Thy/document/Interfaces.tex	Sun Nov 30 14:03:46 2008 +0100
     1.3 @@ -0,0 +1,115 @@
     1.4 +%
     1.5 +\begin{isabellebody}%
     1.6 +\def\isabellecontext{Interfaces}%
     1.7 +%
     1.8 +\isadelimtheory
     1.9 +\isanewline
    1.10 +\isanewline
    1.11 +%
    1.12 +\endisadelimtheory
    1.13 +%
    1.14 +\isatagtheory
    1.15 +\isacommand{theory}\isamarkupfalse%
    1.16 +\ Interfaces\isanewline
    1.17 +\isakeyword{imports}\ Pure\isanewline
    1.18 +\isakeyword{begin}%
    1.19 +\endisatagtheory
    1.20 +{\isafoldtheory}%
    1.21 +%
    1.22 +\isadelimtheory
    1.23 +%
    1.24 +\endisadelimtheory
    1.25 +%
    1.26 +\isamarkupchapter{User interfaces%
    1.27 +}
    1.28 +\isamarkuptrue%
    1.29 +%
    1.30 +\isamarkupsection{Plain TTY interaction \label{sec:tool-tty}%
    1.31 +}
    1.32 +\isamarkuptrue%
    1.33 +%
    1.34 +\begin{isamarkuptext}%
    1.35 +The \indexdef{}{tool}{tty}\hypertarget{tool.tty}{\hyperlink{tool.tty}{\mbox{\isa{\isatt{tty}}}}} tool runs the Isabelle process interactively
    1.36 +  within a plain terminal session:
    1.37 +\begin{ttbox}
    1.38 +Usage: tty [OPTIONS]
    1.39 +
    1.40 +  Options are:
    1.41 +    -l NAME      logic image name (default ISABELLE_LOGIC)
    1.42 +    -m MODE      add print mode for output
    1.43 +    -p NAME      line editor program name (default ISABELLE_LINE_EDITOR)
    1.44 +
    1.45 +  Run Isabelle process with plain tty interaction, and optional line editor.
    1.46 +\end{ttbox}
    1.47 +
    1.48 +  The \verb|-l| option specifies the logic image.  The
    1.49 +  \verb|-m| option specifies additional print modes.  The The
    1.50 +  \verb|-p| option specifies an alternative line editor (such
    1.51 +  as the \indexdef{}{executable}{rlwrap}\hypertarget{executable.rlwrap}{\hyperlink{executable.rlwrap}{\mbox{\isa{\isatt{rlwrap}}}}} wrapper for GNU readline); the
    1.52 +  fall-back is to use raw standard input.
    1.53 +
    1.54 +  Regular interaction is via the standard Isabelle/Isar toplevel loop.
    1.55 +  The Isar command \hyperlink{command.exit}{\mbox{\isa{\isacommand{exit}}}} drops out into the raw ML system,
    1.56 +  which is occasionally useful for low-level debugging.  Invoking \verb|Isar.loop|~\verb|();| in ML will return to the Isar toplevel.%
    1.57 +\end{isamarkuptext}%
    1.58 +\isamarkuptrue%
    1.59 +%
    1.60 +\isamarkupsection{Proof General / Emacs%
    1.61 +}
    1.62 +\isamarkuptrue%
    1.63 +%
    1.64 +\begin{isamarkuptext}%
    1.65 +The \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatt{emacs}}}}} tool invokes a version of Emacs and Proof
    1.66 +  General within the regular Isabelle settings environment
    1.67 +  (\secref{sec:settings}).  This is more robust than starting Emacs
    1.68 +  separately, loading the Proof General lisp files, and then
    1.69 +  attempting to start Isabelle with dynamic \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}} lookup
    1.70 +  etc.
    1.71 +
    1.72 +  The actual interface script is part of the Proof General
    1.73 +  distribution~\cite{proofgeneral}; its usage depends on the
    1.74 +  particular version.  There are some options available, such as
    1.75 +  \verb|-l| for passing the logic image to be used by default,
    1.76 +  or \verb|-m| to tune the standard print mode.  The following
    1.77 +  Isabelle settings are particularly important for Proof General:
    1.78 +
    1.79 +  \begin{description}
    1.80 +
    1.81 +  \item[\indexdef{}{setting}{PROOFGENERAL\_HOME}\hypertarget{setting.PROOFGENERAL-HOME}{\hyperlink{setting.PROOFGENERAL-HOME}{\mbox{\isa{\isatt{PROOFGENERAL{\isacharunderscore}HOME}}}}}] points to the main
    1.82 +  installation directory of the Proof General distribution.  The
    1.83 +  default settings try to locate this in a number of standard places,
    1.84 +  notably \verb|$ISABELLE_HOME/contrib/ProofGeneral|.
    1.85 +
    1.86 +  \item[\indexdef{}{setting}{PROOFGENERAL\_OPTIONS}\hypertarget{setting.PROOFGENERAL-OPTIONS}{\hyperlink{setting.PROOFGENERAL-OPTIONS}{\mbox{\isa{\isatt{PROOFGENERAL{\isacharunderscore}OPTIONS}}}}}] is implicitly prefixed to
    1.87 +  the command line of any invocation of the Proof General \verb|interface| script.
    1.88 +
    1.89 +  \item[\indexdef{}{setting}{XSYMBOL\_INSTALLFONTS}\hypertarget{setting.XSYMBOL-INSTALLFONTS}{\hyperlink{setting.XSYMBOL-INSTALLFONTS}{\mbox{\isa{\isatt{XSYMBOL{\isacharunderscore}INSTALLFONTS}}}}}] may contain a small shell
    1.90 +  script to install the X11 fonts required for the X-Symbols mode of
    1.91 +  Proof General.  This is only relevant if the X11 display server runs
    1.92 +  on a different machine than the Emacs application, with a different
    1.93 +  file-system view on the Proof General installation.  Under most
    1.94 +  circumstances Proof General is able to refer to the font files that
    1.95 +  are part of its distribution.
    1.96 +
    1.97 +  \end{description}%
    1.98 +\end{isamarkuptext}%
    1.99 +\isamarkuptrue%
   1.100 +%
   1.101 +\isadelimtheory
   1.102 +%
   1.103 +\endisadelimtheory
   1.104 +%
   1.105 +\isatagtheory
   1.106 +\isacommand{end}\isamarkupfalse%
   1.107 +%
   1.108 +\endisatagtheory
   1.109 +{\isafoldtheory}%
   1.110 +%
   1.111 +\isadelimtheory
   1.112 +%
   1.113 +\endisadelimtheory
   1.114 +\end{isabellebody}%
   1.115 +%%% Local Variables:
   1.116 +%%% mode: latex
   1.117 +%%% TeX-master: "root"
   1.118 +%%% End: