257 |
257 |
258 The \texttt{-c} option causes the input file to be removed after use. The |
258 The \texttt{-c} option causes the input file to be removed after use. The |
259 printer spool command is determined by the \texttt{PRINT_COMMAND} setting. |
259 printer spool command is determined by the \texttt{PRINT_COMMAND} setting. |
260 |
260 |
261 |
261 |
|
262 \section{Run Isabelle with plain tty interaction --- \texttt{isatool tty}} \label{sec:tool-tty} |
|
263 |
|
264 The \tooldx{tty} utility runs the Isabelle process interactively |
|
265 within a plain terminal session: |
|
266 \begin{ttbox} |
|
267 Usage: tty [OPTIONS] |
|
268 |
|
269 Options are: |
|
270 -l NAME logic image name (default ISABELLE_LOGIC) |
|
271 -m MODE add print mode for output |
|
272 -p NAME line editor program name (default ISABELLE_LINE_EDITOR) |
|
273 |
|
274 Run Isabelle process with plain tty interaction, and optional line editor. |
|
275 \end{ttbox} |
|
276 |
|
277 The \texttt{-l} option specifies the logic image. The \texttt{-m} |
|
278 option specifies additional print modes. The The \texttt{-p} option |
|
279 specifies an alternative line editor (such as the \texttt{rlwrap} |
|
280 wrapper for GNU readline); the fall-back is to use raw standard input. |
|
281 |
|
282 |
262 \section{Remove awkward symbol names from theory sources --- \texttt{isatool unsymbolize}} |
283 \section{Remove awkward symbol names from theory sources --- \texttt{isatool unsymbolize}} |
263 |
284 |
264 The \tooldx{unsymbolize} utility tunes Isabelle theory sources to improve |
285 The \tooldx{unsymbolize} utility tunes Isabelle theory sources to improve |
265 readability for plain ASCII output (e.g.\ in email communication). Most |
286 readability for plain ASCII output (e.g.\ in email communication). Most |
266 notably, \texttt{unsymbolize} replaces awkward arrow symbols such as |
287 notably, \texttt{unsymbolize} replaces awkward arrow symbols such as |
280 |
301 |
281 The \tooldx{version} utility outputs the full version string of the |
302 The \tooldx{version} utility outputs the full version string of the |
282 Isabelle distribution being used, e.g.\ ``\texttt{Isabelle2007: |
303 Isabelle distribution being used, e.g.\ ``\texttt{Isabelle2007: |
283 November 2007}''. There are no options nor arguments. |
304 November 2007}''. There are no options nor arguments. |
284 |
305 |
|
306 |
285 %%% Local Variables: |
307 %%% Local Variables: |
286 %%% mode: latex |
308 %%% mode: latex |
287 %%% TeX-master: "system" |
309 %%% TeX-master: "system" |
288 %%% End: |
310 %%% End: |