99 Usage: isabelle tty [OPTIONS] |
99 Usage: isabelle tty [OPTIONS] |
100 |
100 |
101 Options are: |
101 Options are: |
102 -l NAME logic image name (default ISABELLE_LOGIC) |
102 -l NAME logic image name (default ISABELLE_LOGIC) |
103 -m MODE add print mode for output |
103 -m MODE add print mode for output |
|
104 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
104 -p NAME line editor program name (default ISABELLE_LINE_EDITOR) |
105 -p NAME line editor program name (default ISABELLE_LINE_EDITOR) |
105 |
106 |
106 Run Isabelle process with plain tty interaction and line editor. |
107 Run Isabelle process with plain tty interaction and line editor. |
107 \end{ttbox} |
108 \end{ttbox} |
108 |
109 |
109 The @{verbatim "-l"} option specifies the logic image. The |
110 The @{verbatim "-l"} option specifies the logic image. The |
110 @{verbatim "-m"} option specifies additional print modes. The |
111 @{verbatim "-m"} option specifies additional print modes. The |
111 @{verbatim "-p"} option specifies an alternative line editor (such |
112 @{verbatim "-p"} option specifies an alternative line editor (such |
112 as the @{executable_def rlwrap} wrapper for GNU readline); the |
113 as the @{executable_def rlwrap} wrapper for GNU readline); the |
113 fall-back is to use raw standard input. |
114 fall-back is to use raw standard input. |
|
115 |
|
116 \medskip Option @{verbatim "-o"} allows to override Isabelle system |
|
117 options for this process, see also \secref{sec:system-options}. |
114 |
118 |
115 Regular interaction works via the standard Isabelle/Isar toplevel |
119 Regular interaction works via the standard Isabelle/Isar toplevel |
116 loop. The Isar command @{command exit} drops out into the |
120 loop. The Isar command @{command exit} drops out into the |
117 bare-bones ML system, which is occasionally useful for debugging of |
121 bare-bones ML system, which is occasionally useful for debugging of |
118 the Isar infrastructure itself. Invoking @{ML Isar.loop}~@{verbatim |
122 the Isar infrastructure itself. Invoking @{ML Isar.loop}~@{verbatim |