doc-src/System/Thy/document/Interfaces.tex
author wenzelm
Sun Nov 30 14:03:46 2008 +0100 (2008-11-30)
changeset 28916 0a802cdda340
child 32088 2110fcd86efb
permissions -rw-r--r--
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
separate chapter on interfaces as Isabelle tools;
wenzelm@28916
     1
%
wenzelm@28916
     2
\begin{isabellebody}%
wenzelm@28916
     3
\def\isabellecontext{Interfaces}%
wenzelm@28916
     4
%
wenzelm@28916
     5
\isadelimtheory
wenzelm@28916
     6
\isanewline
wenzelm@28916
     7
\isanewline
wenzelm@28916
     8
%
wenzelm@28916
     9
\endisadelimtheory
wenzelm@28916
    10
%
wenzelm@28916
    11
\isatagtheory
wenzelm@28916
    12
\isacommand{theory}\isamarkupfalse%
wenzelm@28916
    13
\ Interfaces\isanewline
wenzelm@28916
    14
\isakeyword{imports}\ Pure\isanewline
wenzelm@28916
    15
\isakeyword{begin}%
wenzelm@28916
    16
\endisatagtheory
wenzelm@28916
    17
{\isafoldtheory}%
wenzelm@28916
    18
%
wenzelm@28916
    19
\isadelimtheory
wenzelm@28916
    20
%
wenzelm@28916
    21
\endisadelimtheory
wenzelm@28916
    22
%
wenzelm@28916
    23
\isamarkupchapter{User interfaces%
wenzelm@28916
    24
}
wenzelm@28916
    25
\isamarkuptrue%
wenzelm@28916
    26
%
wenzelm@28916
    27
\isamarkupsection{Plain TTY interaction \label{sec:tool-tty}%
wenzelm@28916
    28
}
wenzelm@28916
    29
\isamarkuptrue%
wenzelm@28916
    30
%
wenzelm@28916
    31
\begin{isamarkuptext}%
wenzelm@28916
    32
The \indexdef{}{tool}{tty}\hypertarget{tool.tty}{\hyperlink{tool.tty}{\mbox{\isa{\isatt{tty}}}}} tool runs the Isabelle process interactively
wenzelm@28916
    33
  within a plain terminal session:
wenzelm@28916
    34
\begin{ttbox}
wenzelm@28916
    35
Usage: tty [OPTIONS]
wenzelm@28916
    36
wenzelm@28916
    37
  Options are:
wenzelm@28916
    38
    -l NAME      logic image name (default ISABELLE_LOGIC)
wenzelm@28916
    39
    -m MODE      add print mode for output
wenzelm@28916
    40
    -p NAME      line editor program name (default ISABELLE_LINE_EDITOR)
wenzelm@28916
    41
wenzelm@28916
    42
  Run Isabelle process with plain tty interaction, and optional line editor.
wenzelm@28916
    43
\end{ttbox}
wenzelm@28916
    44
wenzelm@28916
    45
  The \verb|-l| option specifies the logic image.  The
wenzelm@28916
    46
  \verb|-m| option specifies additional print modes.  The The
wenzelm@28916
    47
  \verb|-p| option specifies an alternative line editor (such
wenzelm@28916
    48
  as the \indexdef{}{executable}{rlwrap}\hypertarget{executable.rlwrap}{\hyperlink{executable.rlwrap}{\mbox{\isa{\isatt{rlwrap}}}}} wrapper for GNU readline); the
wenzelm@28916
    49
  fall-back is to use raw standard input.
wenzelm@28916
    50
wenzelm@28916
    51
  Regular interaction is via the standard Isabelle/Isar toplevel loop.
wenzelm@28916
    52
  The Isar command \hyperlink{command.exit}{\mbox{\isa{\isacommand{exit}}}} drops out into the raw ML system,
wenzelm@28916
    53
  which is occasionally useful for low-level debugging.  Invoking \verb|Isar.loop|~\verb|();| in ML will return to the Isar toplevel.%
wenzelm@28916
    54
\end{isamarkuptext}%
wenzelm@28916
    55
\isamarkuptrue%
wenzelm@28916
    56
%
wenzelm@28916
    57
\isamarkupsection{Proof General / Emacs%
wenzelm@28916
    58
}
wenzelm@28916
    59
\isamarkuptrue%
wenzelm@28916
    60
%
wenzelm@28916
    61
\begin{isamarkuptext}%
wenzelm@28916
    62
The \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatt{emacs}}}}} tool invokes a version of Emacs and Proof
wenzelm@28916
    63
  General within the regular Isabelle settings environment
wenzelm@28916
    64
  (\secref{sec:settings}).  This is more robust than starting Emacs
wenzelm@28916
    65
  separately, loading the Proof General lisp files, and then
wenzelm@28916
    66
  attempting to start Isabelle with dynamic \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}} lookup
wenzelm@28916
    67
  etc.
wenzelm@28916
    68
wenzelm@28916
    69
  The actual interface script is part of the Proof General
wenzelm@28916
    70
  distribution~\cite{proofgeneral}; its usage depends on the
wenzelm@28916
    71
  particular version.  There are some options available, such as
wenzelm@28916
    72
  \verb|-l| for passing the logic image to be used by default,
wenzelm@28916
    73
  or \verb|-m| to tune the standard print mode.  The following
wenzelm@28916
    74
  Isabelle settings are particularly important for Proof General:
wenzelm@28916
    75
wenzelm@28916
    76
  \begin{description}
wenzelm@28916
    77
wenzelm@28916
    78
  \item[\indexdef{}{setting}{PROOFGENERAL\_HOME}\hypertarget{setting.PROOFGENERAL-HOME}{\hyperlink{setting.PROOFGENERAL-HOME}{\mbox{\isa{\isatt{PROOFGENERAL{\isacharunderscore}HOME}}}}}] points to the main
wenzelm@28916
    79
  installation directory of the Proof General distribution.  The
wenzelm@28916
    80
  default settings try to locate this in a number of standard places,
wenzelm@28916
    81
  notably \verb|$ISABELLE_HOME/contrib/ProofGeneral|.
wenzelm@28916
    82
wenzelm@28916
    83
  \item[\indexdef{}{setting}{PROOFGENERAL\_OPTIONS}\hypertarget{setting.PROOFGENERAL-OPTIONS}{\hyperlink{setting.PROOFGENERAL-OPTIONS}{\mbox{\isa{\isatt{PROOFGENERAL{\isacharunderscore}OPTIONS}}}}}] is implicitly prefixed to
wenzelm@28916
    84
  the command line of any invocation of the Proof General \verb|interface| script.
wenzelm@28916
    85
wenzelm@28916
    86
  \item[\indexdef{}{setting}{XSYMBOL\_INSTALLFONTS}\hypertarget{setting.XSYMBOL-INSTALLFONTS}{\hyperlink{setting.XSYMBOL-INSTALLFONTS}{\mbox{\isa{\isatt{XSYMBOL{\isacharunderscore}INSTALLFONTS}}}}}] may contain a small shell
wenzelm@28916
    87
  script to install the X11 fonts required for the X-Symbols mode of
wenzelm@28916
    88
  Proof General.  This is only relevant if the X11 display server runs
wenzelm@28916
    89
  on a different machine than the Emacs application, with a different
wenzelm@28916
    90
  file-system view on the Proof General installation.  Under most
wenzelm@28916
    91
  circumstances Proof General is able to refer to the font files that
wenzelm@28916
    92
  are part of its distribution.
wenzelm@28916
    93
wenzelm@28916
    94
  \end{description}%
wenzelm@28916
    95
\end{isamarkuptext}%
wenzelm@28916
    96
\isamarkuptrue%
wenzelm@28916
    97
%
wenzelm@28916
    98
\isadelimtheory
wenzelm@28916
    99
%
wenzelm@28916
   100
\endisadelimtheory
wenzelm@28916
   101
%
wenzelm@28916
   102
\isatagtheory
wenzelm@28916
   103
\isacommand{end}\isamarkupfalse%
wenzelm@28916
   104
%
wenzelm@28916
   105
\endisatagtheory
wenzelm@28916
   106
{\isafoldtheory}%
wenzelm@28916
   107
%
wenzelm@28916
   108
\isadelimtheory
wenzelm@28916
   109
%
wenzelm@28916
   110
\endisadelimtheory
wenzelm@28916
   111
\end{isabellebody}%
wenzelm@28916
   112
%%% Local Variables:
wenzelm@28916
   113
%%% mode: latex
wenzelm@28916
   114
%%% TeX-master: "root"
wenzelm@28916
   115
%%% End: