# HG changeset patch
# User wenzelm
# Date 1343651352 -7200
# Node ID a37463482e5f64644e5acf919b5afe226f97dc8b
# Parent  342ca8f3197bcccf795dd0df5c9cdaa080eb9212
discontinued unused isabelle jedit debugger;
tuned;

diff -r 342ca8f3197b -r a37463482e5f doc-src/System/Thy/Interfaces.thy
--- 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.  *}
 
 
 
diff -r 342ca8f3197b -r a37463482e5f doc-src/System/Thy/document/Interfaces.tex
--- 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%
 %
diff -r 342ca8f3197b -r a37463482e5f src/Tools/jEdit/lib/Tools/jedit
--- 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"
         ;;