equal
deleted
inserted
replaced
219 usage is: |
219 usage is: |
220 \begin{ttbox} |
220 \begin{ttbox} |
221 Usage: isabelle [OPTIONS] [INPUT] [OUTPUT] |
221 Usage: isabelle [OPTIONS] [INPUT] [OUTPUT] |
222 |
222 |
223 Options are: |
223 Options are: |
|
224 -I startup Isar interaction mode |
224 -e MLTEXT pass MLTEXT to the ML session |
225 -e MLTEXT pass MLTEXT to the ML session |
225 -m MODE add print mode for output |
226 -m MODE add print mode for output |
226 -q non-interactive session |
227 -q non-interactive session |
227 -r open heap file read-only |
228 -r open heap file read-only |
228 -u pass 'use"ROOT.ML";' to the ML session |
229 -u pass 'use"ROOT.ML";' to the ML session |
272 \medskip The \texttt{-m} option adds identifiers of print modes to be |
273 \medskip The \texttt{-m} option adds identifiers of print modes to be |
273 made active for this session. Typically, this is used by some user |
274 made active for this session. Typically, this is used by some user |
274 interface, for example to enable output of mathematical symbols from a |
275 interface, for example to enable output of mathematical symbols from a |
275 special screen font. |
276 special screen font. |
276 |
277 |
277 \medskip Isabelle normally enters an interactice {\ML} top-level loop |
278 \medskip Isabelle normally enters an interactice top-level loop (after |
278 (after processing the \texttt{-e} texts). The \texttt{-q} option |
279 processing the \texttt{-e} texts). The \texttt{-q} option inhibits this, thus |
279 inhibits this, thus providing a pure batch mode facility. |
280 providing a pure batch mode facility. |
|
281 |
|
282 \medskip The \texttt{-I} option makes Isabelle enter Isar interaction mode on |
|
283 startup, instead of the primitive {\ML} top-level. This flag is usually |
|
284 enabled by default when running Isabelle via some user interface, but it is |
|
285 \emph{not} for the basic \texttt{isabelle} program. |
280 |
286 |
281 |
287 |
282 \subsection*{Examples} |
288 \subsection*{Examples} |
283 |
289 |
284 Run an interactive session of the default object-logic (as specified |
290 Run an interactive session of the default object-logic (as specified |