--- a/doc-src/System/Thy/Interfaces.thy Sat Jul 28 12:59:53 2012 +0200
+++ b/doc-src/System/Thy/Interfaces.thy Sat Jul 28 13:01:48 2012 +0200
@@ -4,33 +4,44 @@
chapter {* User interfaces *}
-section {* Plain TTY interaction \label{sec:tool-tty} *}
+section {* Isabelle/jEdit Prover IDE \label{sec:tool-jedit} *}
-text {*
- The @{tool_def tty} tool runs the Isabelle process interactively
- within a plain terminal session:
+text {* The @{tool_def jedit} tool invokes a version of jEdit that has
+ been augmented with some components to provide a fully-featured
+ Prover IDE (based on Isabelle/Scala):
\begin{ttbox}
-Usage: isabelle tty [OPTIONS]
+Usage: isabelle jedit [OPTIONS] [FILES ...]
Options are:
+ -J OPTION add JVM runtime option (default JEDIT_JAVA_OPTIONS)
+ -b build only
+ -d enable debugger
+ -f fresh build
+ -j OPTION add jEdit runtime option (default JEDIT_OPTIONS)
-l NAME logic image name (default ISABELLE_LOGIC)
-m MODE add print mode for output
- -p NAME line editor program name (default ISABELLE_LINE_EDITOR)
- Run Isabelle process with plain tty interaction and line editor.
+Start jEdit with Isabelle plugin setup and opens theory FILES
+(default Scratch.thy).
\end{ttbox}
The @{verbatim "-l"} option specifies the logic image. The
- @{verbatim "-m"} option specifies additional print modes. The
- @{verbatim "-p"} option specifies an alternative line editor (such
- as the @{executable_def rlwrap} wrapper for GNU readline); the
- fall-back is to use raw standard input.
+ @{verbatim "-m"} option specifies additional print modes.
+
+ The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass
+ additional low-level options to the JVM or jEdit, respectively. The
+ defaults are provided by the Isabelle settings environment.
- Regular interaction is via the standard Isabelle/Isar toplevel loop.
- The Isar command @{command exit} drops out into the bare-bones ML
- system, which is occasionally useful for debugging of the Isar
- infrastructure itself. Invoking @{ML Isar.loop}~@{verbatim "();"}
- in ML will return to the Isar toplevel. *}
+ The @{verbatim "-d"} option allows to connect to the runtime
+ debugger of the JVM. Note that the Scala Console of Isabelle/jEdit
+ is more convenient in most practical situations.
+
+ The @{verbatim "-b"} and @{verbatim "-f"} options control the
+ self-build mechanism of Isabelle/jEdit. This is only relevant for
+ building from sources, which also requires an auxiliary @{verbatim
+ jedit_build} component. Official Isabelle releases already include
+ a version of Isabelle/jEdit that is built properly.
+*}
section {* Proof General / Emacs *}
@@ -66,43 +77,32 @@
*}
-section {* Isabelle/jEdit Prover IDE \label{sec:tool-jedit} *}
+section {* Plain TTY interaction \label{sec:tool-tty} *}
-text {* The @{tool_def jedit} tool invokes a version of jEdit that has
- been augmented with some components to provide a fully-featured
- Prover IDE (based on Isabelle/Scala):
+text {*
+ The @{tool_def tty} tool runs the Isabelle process interactively
+ within a plain terminal session:
\begin{ttbox}
-Usage: isabelle jedit [OPTIONS] [FILES ...]
+Usage: isabelle tty [OPTIONS]
Options are:
- -J OPTION add JVM runtime option (default JEDIT_JAVA_OPTIONS)
- -b build only
- -d enable debugger
- -f fresh build
- -j OPTION add jEdit runtime option (default JEDIT_OPTIONS)
-l NAME logic image name (default ISABELLE_LOGIC)
-m MODE add print mode for output
+ -p NAME line editor program name (default ISABELLE_LINE_EDITOR)
-Start jEdit with Isabelle plugin setup and opens theory FILES
-(default Scratch.thy).
+ Run Isabelle process with plain tty interaction and line editor.
\end{ttbox}
-The @{verbatim "-l"} option specifies the logic image. The
-@{verbatim "-m"} option specifies additional print modes.
-
-The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass
-additional low-level options to the JVM or jEdit, respectively. The
-defaults are provided by the Isabelle settings environment.
+ The @{verbatim "-l"} option specifies the logic image. The
+ @{verbatim "-m"} option specifies additional print modes. The
+ @{verbatim "-p"} option specifies an alternative line editor (such
+ as the @{executable_def rlwrap} wrapper for GNU readline); the
+ fall-back is to use raw standard input.
-The @{verbatim "-d"} option allows to connect to the runtime debugger
-of the JVM. Note that the Scala Console of Isabelle/jEdit is more
-convenient in most practical situations.
-
-The @{verbatim "-b"} and @{verbatim "-f"} options control the
-self-build mechanism of Isabelle/jEdit. This is only relevant for
-building from sources, which also requires an auxiliary @{verbatim
-jedit_build} component. Official Isabelle releases already include a
-version of Isabelle/jEdit that is built properly.
-*}
+ Regular interaction is via the standard Isabelle/Isar toplevel loop.
+ The Isar command @{command exit} drops out into the bare-bones ML
+ system, which is occasionally useful for debugging of the Isar
+ infrastructure itself. Invoking @{ML Isar.loop}~@{verbatim "();"}
+ in ML will return to the Isar toplevel. *}
end
\ No newline at end of file
--- a/doc-src/System/Thy/document/Interfaces.tex Sat Jul 28 12:59:53 2012 +0200
+++ b/doc-src/System/Thy/document/Interfaces.tex Sat Jul 28 13:01:48 2012 +0200
@@ -22,35 +22,45 @@
}
\isamarkuptrue%
%
-\isamarkupsection{Plain TTY interaction \label{sec:tool-tty}%
+\isamarkupsection{Isabelle/jEdit Prover IDE \label{sec:tool-jedit}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \indexdef{}{tool}{tty}\hypertarget{tool.tty}{\hyperlink{tool.tty}{\mbox{\isa{\isatt{tty}}}}} tool runs the Isabelle process interactively
- within a plain terminal session:
+The \indexdef{}{tool}{jedit}\hypertarget{tool.jedit}{\hyperlink{tool.jedit}{\mbox{\isa{\isatt{jedit}}}}} tool invokes a version of jEdit that has
+ been augmented with some components to provide a fully-featured
+ Prover IDE (based on Isabelle/Scala):
\begin{ttbox}
-Usage: isabelle tty [OPTIONS]
+Usage: isabelle jedit [OPTIONS] [FILES ...]
Options are:
+ -J OPTION add JVM runtime option (default JEDIT_JAVA_OPTIONS)
+ -b build only
+ -d enable debugger
+ -f fresh build
+ -j OPTION add jEdit runtime option (default JEDIT_OPTIONS)
-l NAME logic image name (default ISABELLE_LOGIC)
-m MODE add print mode for output
- -p NAME line editor program name (default ISABELLE_LINE_EDITOR)
- Run Isabelle process with plain tty interaction and line editor.
+Start jEdit with Isabelle plugin setup and opens theory FILES
+(default Scratch.thy).
\end{ttbox}
The \verb|-l| option specifies the logic image. The
- \verb|-m| option specifies additional print modes. The
- \verb|-p| option specifies an alternative line editor (such
- as the \indexdef{}{executable}{rlwrap}\hypertarget{executable.rlwrap}{\hyperlink{executable.rlwrap}{\mbox{\isa{\isatt{rlwrap}}}}} wrapper for GNU readline); the
- fall-back is to use raw standard input.
+ \verb|-m| option specifies additional print modes.
+
+ The \verb|-J| and \verb|-j| options allow to pass
+ additional low-level options to the JVM or jEdit, respectively. The
+ defaults are provided by the Isabelle settings environment.
- Regular interaction is via the standard Isabelle/Isar toplevel loop.
- The Isar command \hyperlink{command.exit}{\mbox{\isa{\isacommand{exit}}}} drops out into the bare-bones ML
- system, which is occasionally useful for debugging of the Isar
- infrastructure itself. Invoking \verb|Isar.loop|~\verb|();|
- in ML will return to the Isar toplevel.%
+ The \verb|-d| option allows to connect to the runtime
+ debugger of the JVM. Note that the Scala Console of Isabelle/jEdit
+ is more convenient in most practical situations.
+
+ The \verb|-b| and \verb|-f| options control the
+ self-build mechanism of Isabelle/jEdit. This is only relevant for
+ building from sources, which also requires an auxiliary \verb|jedit_build| component. Official Isabelle releases already include
+ a version of Isabelle/jEdit that is built properly.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -89,45 +99,35 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Isabelle/jEdit Prover IDE \label{sec:tool-jedit}%
+\isamarkupsection{Plain TTY interaction \label{sec:tool-tty}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \indexdef{}{tool}{jedit}\hypertarget{tool.jedit}{\hyperlink{tool.jedit}{\mbox{\isa{\isatt{jedit}}}}} tool invokes a version of jEdit that has
- been augmented with some components to provide a fully-featured
- Prover IDE (based on Isabelle/Scala):
+The \indexdef{}{tool}{tty}\hypertarget{tool.tty}{\hyperlink{tool.tty}{\mbox{\isa{\isatt{tty}}}}} tool runs the Isabelle process interactively
+ within a plain terminal session:
\begin{ttbox}
-Usage: isabelle jedit [OPTIONS] [FILES ...]
+Usage: isabelle tty [OPTIONS]
Options are:
- -J OPTION add JVM runtime option (default JEDIT_JAVA_OPTIONS)
- -b build only
- -d enable debugger
- -f fresh build
- -j OPTION add jEdit runtime option (default JEDIT_OPTIONS)
-l NAME logic image name (default ISABELLE_LOGIC)
-m MODE add print mode for output
+ -p NAME line editor program name (default ISABELLE_LINE_EDITOR)
-Start jEdit with Isabelle plugin setup and opens theory FILES
-(default Scratch.thy).
+ Run Isabelle process with plain tty interaction and line editor.
\end{ttbox}
-The \verb|-l| option specifies the logic image. The
-\verb|-m| option specifies additional print modes.
-
-The \verb|-J| and \verb|-j| options allow to pass
-additional low-level options to the JVM or jEdit, respectively. The
-defaults are provided by the Isabelle settings environment.
+ The \verb|-l| option specifies the logic image. The
+ \verb|-m| option specifies additional print modes. The
+ \verb|-p| option specifies an alternative line editor (such
+ as the \indexdef{}{executable}{rlwrap}\hypertarget{executable.rlwrap}{\hyperlink{executable.rlwrap}{\mbox{\isa{\isatt{rlwrap}}}}} wrapper for GNU readline); the
+ fall-back is to use raw standard input.
-The \verb|-d| option allows to connect to the runtime debugger
-of the JVM. Note that the Scala Console of Isabelle/jEdit is more
-convenient in most practical situations.
-
-The \verb|-b| and \verb|-f| options control the
-self-build mechanism of Isabelle/jEdit. This is only relevant for
-building from sources, which also requires an auxiliary \verb|jedit_build| component. Official Isabelle releases already include a
-version of Isabelle/jEdit that is built properly.%
+ Regular interaction is via the standard Isabelle/Isar toplevel loop.
+ The Isar command \hyperlink{command.exit}{\mbox{\isa{\isacommand{exit}}}} drops out into the bare-bones ML
+ system, which is occasionally useful for debugging of the Isar
+ infrastructure itself. Invoking \verb|Isar.loop|~\verb|();|
+ in ML will return to the Isar toplevel.%
\end{isamarkuptext}%
\isamarkuptrue%
%