# HG changeset patch
# User wenzelm
# Date 1335625531 -7200
# Node ID 65082431af2a6978b70d16d69dfa6c6540e7fcbe
# Parent  4fad76e6f4ba5654c0027c6a05dd409bc2241331
some coverage of Isabelle/jEdit;

diff -r 4fad76e6f4ba -r 65082431af2a doc-src/System/Thy/Interfaces.thy
--- 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
diff -r 4fad76e6f4ba -r 65082431af2a doc-src/System/Thy/document/Interfaces.tex
--- 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