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