# HG changeset patch # User wenzelm # Date 1343473308 -7200 # Node ID de82a584bc2a59d505ae057cc81978c5bbdb1eef # Parent af0f5560ac94f94fbe34f0b88290146aafbca3c3 top-down order of user interfaces; diff -r af0f5560ac94 -r de82a584bc2a doc-src/System/Thy/Interfaces.thy --- 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 diff -r af0f5560ac94 -r de82a584bc2a doc-src/System/Thy/document/Interfaces.tex --- 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% %