--- a/doc-src/System/Thy/Interfaces.thy Mon Jul 30 14:11:29 2012 +0200
+++ b/doc-src/System/Thy/Interfaces.thy Mon Jul 30 14:29:12 2012 +0200
@@ -6,16 +6,15 @@
section {* Isabelle/jEdit Prover IDE \label{sec:tool-jedit} *}
-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 ...]
+text {* The @{tool_def jedit} tool invokes a version of
+ jEdit\footnote{\url{http://www.jedit.org/}} that has been augmented
+ with some components to provide a fully-featured Prover IDE:
+\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)
@@ -30,28 +29,26 @@
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.
+ defaults are provided by the Isabelle settings environment
+ (\secref{sec:settings}).
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.
-*}
+ jedit_build}
+ component.\footnote{\url{http://isabelle.in.tum.de/components}} Note
+ that official Isabelle releases already include a version of
+ Isabelle/jEdit that is built properly. *}
section {* Proof General / Emacs *}
text {* The @{tool_def emacs} tool invokes a version of Emacs and
- Proof General \cite{proofgeneral} within the regular Isabelle
- settings environment (\secref{sec:settings}). This is more
- convenient than starting Emacs separately, loading the Proof General
- lisp files, and then attempting to start Isabelle with dynamic
- @{setting PATH} lookup etc.
+ Proof General\footnote{http://proofgeneral.inf.ed.ac.uk/} within the
+ regular Isabelle settings environment (\secref{sec:settings}). This
+ is more convenient than starting Emacs separately, loading the Proof
+ General LISP files, and then attempting to start Isabelle with
+ dynamic @{setting PATH} lookup etc.
The actual interface script is part of the Proof General
distribution; its usage depends on the particular version. There
@@ -99,11 +96,11 @@
as the @{executable_def rlwrap} wrapper for GNU readline); the
fall-back is to use raw standard input.
- 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. *}
+ Regular interaction works 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. *}
--- a/doc-src/System/Thy/document/Interfaces.tex Mon Jul 30 14:11:29 2012 +0200
+++ b/doc-src/System/Thy/document/Interfaces.tex Mon Jul 30 14:29:12 2012 +0200
@@ -27,16 +27,15 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \indexdef{}{tool}{jedit}\hypertarget{tool.jedit}{\hyperlink{tool.jedit}{\mbox{\isa{\isatool{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 ...]
+The \indexdef{}{tool}{jedit}\hypertarget{tool.jedit}{\hyperlink{tool.jedit}{\mbox{\isa{\isatool{jedit}}}}} tool invokes a version of
+ jEdit\footnote{\url{http://www.jedit.org/}} that has been augmented
+ with some components to provide a fully-featured Prover IDE:
+\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)
@@ -51,16 +50,15 @@
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.
+ defaults are provided by the Isabelle settings environment
+ (\secref{sec:settings}).
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.%
+ building from sources, which also requires an auxiliary \verb|jedit_build|
+ component.\footnote{\url{http://isabelle.in.tum.de/components}} Note
+ that official Isabelle releases already include a version of
+ Isabelle/jEdit that is built properly.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -70,11 +68,11 @@
%
\begin{isamarkuptext}%
The \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatool{emacs}}}}} tool invokes a version of Emacs and
- Proof General \cite{proofgeneral} within the regular Isabelle
- settings environment (\secref{sec:settings}). This is more
- convenient than starting Emacs separately, loading the Proof General
- lisp files, and then attempting to start Isabelle with dynamic
- \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}} lookup etc.
+ Proof General\footnote{http://proofgeneral.inf.ed.ac.uk/} within the
+ regular Isabelle settings environment (\secref{sec:settings}). This
+ is more convenient than starting Emacs separately, loading the Proof
+ General LISP files, and then attempting to start Isabelle with
+ dynamic \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}} lookup etc.
The actual interface script is part of the Proof General
distribution; its usage depends on the particular version. There
@@ -123,11 +121,10 @@
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.
- 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.%
+ Regular interaction works 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%
%
--- a/src/Tools/jEdit/lib/Tools/jedit Mon Jul 30 14:11:29 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Mon Jul 30 14:29:12 2012 +0200
@@ -52,7 +52,6 @@
echo " -J OPTION add JVM runtime option"
echo " (default JEDIT_JAVA_OPTIONS=$JEDIT_JAVA_OPTIONS)"
echo " -b build only"
- echo " -d enable debugger"
echo " -f fresh build"
echo " -j OPTION add jEdit runtime option"
echo " (default JEDIT_OPTIONS=$JEDIT_OPTIONS)"
@@ -98,10 +97,6 @@
b)
BUILD_ONLY=true
;;
- d)
- JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Xdebug"
- JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Xrunjdwp:transport=dt_socket,server=y,suspend=n"
- ;;
f)
BUILD_JARS="jars_fresh"
;;