--- a/doc-src/System/Thy/Interfaces.thy Sat Apr 28 16:44:32 2012 +0200
+++ b/doc-src/System/Thy/Interfaces.thy Sat Apr 28 17:05:31 2012 +0200
@@ -21,7 +21,7 @@
\end{ttbox}
The @{verbatim "-l"} option specifies the logic image. The
- @{verbatim "-m"} option specifies additional print modes. The 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.
@@ -73,4 +73,44 @@
\end{description}
*}
+
+section {* Isabelle/jEdit Prover IDE *}
+
+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 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
+
+Start jEdit with Isabelle plugin setup and opens theory FILES
+(default Scratch.thy).
+\end{ttbox}
+
+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 "-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.
+
+The @{verbatim "-l"} option specifies the logic image. The
+@{verbatim "-m"} option specifies additional print modes.
+*}
+
end
\ No newline at end of file
--- a/doc-src/System/Thy/document/Interfaces.tex Sat Apr 28 16:44:32 2012 +0200
+++ b/doc-src/System/Thy/document/Interfaces.tex Sat Apr 28 17:05:31 2012 +0200
@@ -41,7 +41,7 @@
\end{ttbox}
The \verb|-l| option specifies the logic image. The
- \verb|-m| option specifies additional print modes. The 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.
@@ -94,6 +94,48 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsection{Isabelle/jEdit Prover IDE%
+}
+\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):
+\begin{ttbox}
+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
+
+Start jEdit with Isabelle plugin setup and opens theory FILES
+(default Scratch.thy).
+\end{ttbox}
+
+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|-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.
+
+The \verb|-l| option specifies the logic image. The
+\verb|-m| option specifies additional print modes.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isadelimtheory
%
\endisadelimtheory