1.1 --- a/doc-src/System/Thy/Interfaces.thy Mon Jul 30 14:11:29 2012 +0200
1.2 +++ b/doc-src/System/Thy/Interfaces.thy Mon Jul 30 14:29:12 2012 +0200
1.3 @@ -6,16 +6,15 @@
1.4
1.5 section {* Isabelle/jEdit Prover IDE \label{sec:tool-jedit} *}
1.6
1.7 -text {* The @{tool_def jedit} tool invokes a version of jEdit that has
1.8 - been augmented with some components to provide a fully-featured
1.9 - Prover IDE (based on Isabelle/Scala):
1.10 -\begin{ttbox}
1.11 -Usage: isabelle jedit [OPTIONS] [FILES ...]
1.12 +text {* The @{tool_def jedit} tool invokes a version of
1.13 + jEdit\footnote{\url{http://www.jedit.org/}} that has been augmented
1.14 + with some components to provide a fully-featured Prover IDE:
1.15 +\begin{ttbox} Usage: isabelle jedit [OPTIONS]
1.16 + [FILES ...]
1.17
1.18 Options are:
1.19 -J OPTION add JVM runtime option (default JEDIT_JAVA_OPTIONS)
1.20 -b build only
1.21 - -d enable debugger
1.22 -f fresh build
1.23 -j OPTION add jEdit runtime option (default JEDIT_OPTIONS)
1.24 -l NAME logic image name (default ISABELLE_LOGIC)
1.25 @@ -30,28 +29,26 @@
1.26
1.27 The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass
1.28 additional low-level options to the JVM or jEdit, respectively. The
1.29 - defaults are provided by the Isabelle settings environment.
1.30 -
1.31 - The @{verbatim "-d"} option allows to connect to the runtime
1.32 - debugger of the JVM. Note that the Scala Console of Isabelle/jEdit
1.33 - is more convenient in most practical situations.
1.34 + defaults are provided by the Isabelle settings environment
1.35 + (\secref{sec:settings}).
1.36
1.37 The @{verbatim "-b"} and @{verbatim "-f"} options control the
1.38 self-build mechanism of Isabelle/jEdit. This is only relevant for
1.39 building from sources, which also requires an auxiliary @{verbatim
1.40 - jedit_build} component. Official Isabelle releases already include
1.41 - a version of Isabelle/jEdit that is built properly.
1.42 -*}
1.43 + jedit_build}
1.44 + component.\footnote{\url{http://isabelle.in.tum.de/components}} Note
1.45 + that official Isabelle releases already include a version of
1.46 + Isabelle/jEdit that is built properly. *}
1.47
1.48
1.49 section {* Proof General / Emacs *}
1.50
1.51 text {* The @{tool_def emacs} tool invokes a version of Emacs and
1.52 - Proof General \cite{proofgeneral} within the regular Isabelle
1.53 - settings environment (\secref{sec:settings}). This is more
1.54 - convenient than starting Emacs separately, loading the Proof General
1.55 - lisp files, and then attempting to start Isabelle with dynamic
1.56 - @{setting PATH} lookup etc.
1.57 + Proof General\footnote{http://proofgeneral.inf.ed.ac.uk/} within the
1.58 + regular Isabelle settings environment (\secref{sec:settings}). This
1.59 + is more convenient than starting Emacs separately, loading the Proof
1.60 + General LISP files, and then attempting to start Isabelle with
1.61 + dynamic @{setting PATH} lookup etc.
1.62
1.63 The actual interface script is part of the Proof General
1.64 distribution; its usage depends on the particular version. There
1.65 @@ -99,11 +96,11 @@
1.66 as the @{executable_def rlwrap} wrapper for GNU readline); the
1.67 fall-back is to use raw standard input.
1.68
1.69 - Regular interaction is via the standard Isabelle/Isar toplevel loop.
1.70 - The Isar command @{command exit} drops out into the bare-bones ML
1.71 - system, which is occasionally useful for debugging of the Isar
1.72 - infrastructure itself. Invoking @{ML Isar.loop}~@{verbatim "();"}
1.73 - in ML will return to the Isar toplevel. *}
1.74 + Regular interaction works via the standard Isabelle/Isar toplevel
1.75 + loop. The Isar command @{command exit} drops out into the
1.76 + bare-bones ML system, which is occasionally useful for debugging of
1.77 + the Isar infrastructure itself. Invoking @{ML Isar.loop}~@{verbatim
1.78 + "();"} in ML will return to the Isar toplevel. *}
1.79
1.80
1.81
2.1 --- a/doc-src/System/Thy/document/Interfaces.tex Mon Jul 30 14:11:29 2012 +0200
2.2 +++ b/doc-src/System/Thy/document/Interfaces.tex Mon Jul 30 14:29:12 2012 +0200
2.3 @@ -27,16 +27,15 @@
2.4 \isamarkuptrue%
2.5 %
2.6 \begin{isamarkuptext}%
2.7 -The \indexdef{}{tool}{jedit}\hypertarget{tool.jedit}{\hyperlink{tool.jedit}{\mbox{\isa{\isatool{jedit}}}}} tool invokes a version of jEdit that has
2.8 - been augmented with some components to provide a fully-featured
2.9 - Prover IDE (based on Isabelle/Scala):
2.10 -\begin{ttbox}
2.11 -Usage: isabelle jedit [OPTIONS] [FILES ...]
2.12 +The \indexdef{}{tool}{jedit}\hypertarget{tool.jedit}{\hyperlink{tool.jedit}{\mbox{\isa{\isatool{jedit}}}}} tool invokes a version of
2.13 + jEdit\footnote{\url{http://www.jedit.org/}} that has been augmented
2.14 + with some components to provide a fully-featured Prover IDE:
2.15 +\begin{ttbox} Usage: isabelle jedit [OPTIONS]
2.16 + [FILES ...]
2.17
2.18 Options are:
2.19 -J OPTION add JVM runtime option (default JEDIT_JAVA_OPTIONS)
2.20 -b build only
2.21 - -d enable debugger
2.22 -f fresh build
2.23 -j OPTION add jEdit runtime option (default JEDIT_OPTIONS)
2.24 -l NAME logic image name (default ISABELLE_LOGIC)
2.25 @@ -51,16 +50,15 @@
2.26
2.27 The \verb|-J| and \verb|-j| options allow to pass
2.28 additional low-level options to the JVM or jEdit, respectively. The
2.29 - defaults are provided by the Isabelle settings environment.
2.30 -
2.31 - The \verb|-d| option allows to connect to the runtime
2.32 - debugger of the JVM. Note that the Scala Console of Isabelle/jEdit
2.33 - is more convenient in most practical situations.
2.34 + defaults are provided by the Isabelle settings environment
2.35 + (\secref{sec:settings}).
2.36
2.37 The \verb|-b| and \verb|-f| options control the
2.38 self-build mechanism of Isabelle/jEdit. This is only relevant for
2.39 - building from sources, which also requires an auxiliary \verb|jedit_build| component. Official Isabelle releases already include
2.40 - a version of Isabelle/jEdit that is built properly.%
2.41 + building from sources, which also requires an auxiliary \verb|jedit_build|
2.42 + component.\footnote{\url{http://isabelle.in.tum.de/components}} Note
2.43 + that official Isabelle releases already include a version of
2.44 + Isabelle/jEdit that is built properly.%
2.45 \end{isamarkuptext}%
2.46 \isamarkuptrue%
2.47 %
2.48 @@ -70,11 +68,11 @@
2.49 %
2.50 \begin{isamarkuptext}%
2.51 The \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatool{emacs}}}}} tool invokes a version of Emacs and
2.52 - Proof General \cite{proofgeneral} within the regular Isabelle
2.53 - settings environment (\secref{sec:settings}). This is more
2.54 - convenient than starting Emacs separately, loading the Proof General
2.55 - lisp files, and then attempting to start Isabelle with dynamic
2.56 - \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}} lookup etc.
2.57 + Proof General\footnote{http://proofgeneral.inf.ed.ac.uk/} within the
2.58 + regular Isabelle settings environment (\secref{sec:settings}). This
2.59 + is more convenient than starting Emacs separately, loading the Proof
2.60 + General LISP files, and then attempting to start Isabelle with
2.61 + dynamic \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}} lookup etc.
2.62
2.63 The actual interface script is part of the Proof General
2.64 distribution; its usage depends on the particular version. There
2.65 @@ -123,11 +121,10 @@
2.66 as the \indexdef{}{executable}{rlwrap}\hypertarget{executable.rlwrap}{\hyperlink{executable.rlwrap}{\mbox{\isa{\isatt{rlwrap}}}}} wrapper for GNU readline); the
2.67 fall-back is to use raw standard input.
2.68
2.69 - Regular interaction is via the standard Isabelle/Isar toplevel loop.
2.70 - The Isar command \hyperlink{command.exit}{\mbox{\isa{\isacommand{exit}}}} drops out into the bare-bones ML
2.71 - system, which is occasionally useful for debugging of the Isar
2.72 - infrastructure itself. Invoking \verb|Isar.loop|~\verb|();|
2.73 - in ML will return to the Isar toplevel.%
2.74 + Regular interaction works via the standard Isabelle/Isar toplevel
2.75 + loop. The Isar command \hyperlink{command.exit}{\mbox{\isa{\isacommand{exit}}}} drops out into the
2.76 + bare-bones ML system, which is occasionally useful for debugging of
2.77 + the Isar infrastructure itself. Invoking \verb|Isar.loop|~\verb|();| in ML will return to the Isar toplevel.%
2.78 \end{isamarkuptext}%
2.79 \isamarkuptrue%
2.80 %
3.1 --- a/src/Tools/jEdit/lib/Tools/jedit Mon Jul 30 14:11:29 2012 +0200
3.2 +++ b/src/Tools/jEdit/lib/Tools/jedit Mon Jul 30 14:29:12 2012 +0200
3.3 @@ -52,7 +52,6 @@
3.4 echo " -J OPTION add JVM runtime option"
3.5 echo " (default JEDIT_JAVA_OPTIONS=$JEDIT_JAVA_OPTIONS)"
3.6 echo " -b build only"
3.7 - echo " -d enable debugger"
3.8 echo " -f fresh build"
3.9 echo " -j OPTION add jEdit runtime option"
3.10 echo " (default JEDIT_OPTIONS=$JEDIT_OPTIONS)"
3.11 @@ -98,10 +97,6 @@
3.12 b)
3.13 BUILD_ONLY=true
3.14 ;;
3.15 - d)
3.16 - JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Xdebug"
3.17 - JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Xrunjdwp:transport=dt_socket,server=y,suspend=n"
3.18 - ;;
3.19 f)
3.20 BUILD_JARS="jars_fresh"
3.21 ;;